The Infinox Infinity Inferrer - A Complement to Finite Model Finding

Abstract

Infinox is an automated reasoning tool that can disprove the existence of finite models of first-order theories. It is a tool of both theoretical and practical value and is especially well suited as a complement to finite model finders. The main idea behind Infinox is to search for function and predicate symbols with certain properties that imply the non-existence of finite models. A standard automated theorem prover is used to check if these properties hold. We describe the methods used to identify terms that possess the desired properties, and explain in detail how these can be combined and applied to concrete problems. Some very promising first results are presented; Infinox has classified a large number of problems from the TPTP problem library as finitely unsatisfiable. Many of these problems have never before been solved (nor classified) by an automated system.