posted on 2008-06-01, 00:00authored byVijay Chandru, John N. Hooker, Anjul Shrivastava, Gabriela Rago
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.