Oshl-u: a first order theorem prover using propositional techniques and semantics
David A. Plaisted, Swaha Miller · 2005
Automated theorem proving is the proving of theorems with an automatic computer program. Automation of theorem proving is useful in proving repetitive theorems quickly and accurately, as well as in proving theorems that may be too large or complex for humans to handle. Automated theorem proving finds application in various fields, such as, the verification of integrated circuits, software verification, deductive databases, mathematics, and education. The early success of automated theorem provers for first-order logic based on the resolution-unification paradigm has caused theorem proving research to be directed largely towards resolution and its variants. The problems people looked at in the early days of automated deduction were mostly in the classes of problems that resolution is especially efficient at solving such as Horn problems (Every clause in such problems contains at most one positive literal) and UR resolvable problems (Problems in which the proof can be obtained purely by UR resolution, which is a restricted form of resolution). The initially good performance of resolution on such problems led to disillusionment later on. Problems that are hard to solve for humans are less and less likely to be Horn or UR resolvable, so resolution is less likely to be efficient on such problems. That few hard problems have been solved automatically by current provers further supports this. Therefore, there is a need to go beyond resolution for harder problems. Approaches based on propositional techniques applied to first-order theorem proving have great potential in this direction. Provers based on propositional techniques such as DPLL are used extensively for hardware verification but resolution is hardly ever used for solution of large propositional problems because it is far less efficient. Resolution has serious inefficiencies on non-Horn propositional problems and it is likely that these inefficiencies carry over also to first-order problems. In recent times, techniques developed for deciding propositional satisfiability perform at tremendous speeds, solving verification problems containing tens of thousands of variables and hard random 3SAT problems containing millions of variables. The desire to import such propositional efficiency into first-order theorem proving has revived an interest in propositional techniques for proving first-order logic problems. This dissertation explores propositional techniques to first-order theorem proving and how these compare in performance to resolution-unification techniques. It formulates some techniques that are shown to enhance the performance of OSHL, a theorem prover for first-order logic based on propositional techniques. The resulting implementation, OSHL-U, performs better than resolution on categories of problems that are hard for resolution. The performance of OSHL-U can further be improved by the use of semantics that provide problem-specific information to help the proof search; this is demonstrated experimentally in the dissertation. The techniques applied to enhance OSHL performance are applicable to other theorem provers, too, and contribute towards building more powerful theorem provers for first-order logic in general.