Automated Inference of Finite Unsatisfiability

Abstract

We present Infinox, an automated tool for analyzing first-order logic problems, aimed at showing finite unsatisfiability, i.e. the absence of models with finite domains. Finite satisfiability is a semi-decidable problem, which means that such a tool can never be complete. Nevertheless, our hope is that Infinox be a complement to finite model finders in practice. The implementation consists of several different proof techniques for showing infinity of a set, each of which requires the identification of a function or a relation with particular properties. Infinox enumerates candidates to such functions and relations, and subsequently uses an automated theorem prover as a sub-procedure to try to prove the resulting proof obligations. We have evaluated Infinox on the relevant problems from the TPTP benchmark suite, with very promising results.