A Partial Instantiation Based First Order Theorem Prover

Satisfiability algorithms for propositional logic have improved enormously in recent years. This increases the attractiveness of satisfiability methods for first order logic that reduce the problem to a series of ground-level satisfiability problems. Partial Instantiation for first order satisfiability differs radically from standard resolution based methods. Two approaches to partial instantiation based first order theorem provers have been studied by R. Jeroslow and by Plaisted and Zhu. Hooker and Rago have described improvements of Jeroslow's approach by a) extending it to logic with functions b) accelerating it through use of satisfiers as introduced by Gallo and Rago, and c) simplifying it to obtain further speedup. The correctness of the Partial Instantiation algorithms described here for full first-order logic with functions as well as termination on unsatisfiable formulas are shown in [9] This paper describes the implementation of a theorem prover based on the primal algorithm and applied it to solving planning problems as also developed techniques for answer generation when using partial instantiation. We obtained improved efficiency by incorporating incrementality into the primal algorithm (incremental blockage testing). This extended abstract describes the Partial Primal Instantiation algorithm its implementation and preliminary results on first order formulation of planning problems.