Deciding Simple Infinity Axiom Sets with One Binary Relation by Means of Superpostulates

Modern logic engines widely fail to decide axiom sets that are satisfiable only in an infinite domain. This paper specifies an algorithm that automatically generates a database of independent infinity axiom sets with fewer than 1000 characters. It starts with complete theories of pure first-order logic with only one binary relation (FOL[Formula: see text]) and generates further infinity axiom sets S of FOL[Formula: see text] with fewer than 1000 characters such that no other infinity axiom set with fewer than 1000 characters exists in the database that implies S. We call the generated infinity axiom sets S “superpostulates”. Any formula that is derivable from (satisfiable) superpostulates is also satisfiable. Thus far, we have generated a database with 2346 infinity superpostulates by running our algorithm. This paper ends by identifying three practical uses of the algorithmic generation of such a database: (i) for systematic investigations of infinity axiom sets, (ii) for deciding infinity axiom sets and (iii) for the development of saturation algorithms.