Instance-based first-order methods using propositional calculus provers
David A. Plaisted, M. Paramasivam · 1997
Early refutational theorem proving procedures were direct applications of Herbrand's version of the completeness theorem for first-order logic. These instance-based theorem provers created propositional instances of the first-order clauses to be proved unsatisfiable, and tested the instances on a propositional calculus prover. This methodology was not pursued for several decades as it was thought to be too slow. Moreover, the invention of the resolution inference rule changed the direction of theorem proving forever. The success of resolution was largely due to unification. Recently, unification has been incorporated in creating instances of first-order clauses. Furthermore, high-performance propositional calculus provers have been developed in the past few years. As a result, it is possible to realize effective instance-based first-order methods for several applications. We describe the design of instance-based methods for three different purposes. First, RRTP is a theorem prover based on the idea of replacing predicates with their definitions. We compare its performance with some state-of-the-art theorem provers. Second, we describe a proof procedure for Horn theories. The proof procedure creates instances of the input clauses by backward chaining and reasons forward among the instances to find the proof. Third, we describe the construction of a finite-model finder. Finally, we describe the application of the theorem prover and the model finder on an application--description logics. We show by empirical means that, contrary to general belief, theorem provers compare well with specialized application-specific techniques for description logics.