Skip to main content
Article
Partial Instantiation Methods for Inference in First-Order Logic
Journal of Automated Reasoning
  • John N. Hooker, Carnegie Mellon University
  • G. Rago, University of Pisa
  • V. Chandru, Indian Institute of Science, Bangalore
  • A. Shrivastava, Sanchez Computer Associates
Date of Original Version
6-1-2000
Type
Article
Abstract or Description

Satisfiability algorithms for propositional logic have improved enormously in recently years. This improvement increases the attractiveness of satisfiability methods for first-order logic that reduce the problem to a series of ground-level satisfiability problems. R. Jeroslow introduced a partial instantiation method of this kind that differs radically from the standard resolution-based methods. This paper lays the theoretical groundwork for an extension of his method that is general enough and efficient enough for general logic programming with indefinite clauses. In particular we improve Jeroslow's approach by (1) extending it to logic with functions, (2) accelerating it through the use of satisfiers, as introduced by Gallo and Rago, and (3) simplifying it to obtain further speedup. We provide a similar development for a "dual" partial instantiation approach defined by Hooker and suggest a primal–dual strategy. We prove correctness of the primal and dual algorithms for full first-order logic with functions, as well as termination on unsatisfiable formulas. We also report some preliminary computational results.

DOI
10.1023/A:1015854101244
Citation Information
John N. Hooker, G. Rago, V. Chandru and A. Shrivastava. "Partial Instantiation Methods for Inference in First-Order Logic" Journal of Automated Reasoning Vol. 28 (2000) p. 371 - 396
Available at: http://works.bepress.com/jnhooker/83/