ModGen: Theorem Proving by Model Generation

Abstract

ModGen (Model Generation) is a complete theorem prover for first order logic with finite Herbrand domains. ModGen takes first order formulas as input, and generates models of the input formulas. ModGen consists of two major modules: a module for transforming the input formulas into propositional clauses, and a module to find models of the propositional clauses. The first module can be used by other researchers so that the SAT problems can be easily represented, stored and communicated. An important issue in the design of ModGen is to ensure that transformed propositional clauses are satisfiable iff the original formulas are. The second module can be easily replaced by any advanced SAT problem solver. ModGen is easy to use and very efficient. Many problems which are hard for general resolution theorem provers are found easy for ModGen. Introduction Many theorem proving problems are difficult for today 's theorem provers not because these problems are really hard but because the method...