Automatic recognition of tractability in inference relations

ABSTRACT

A procedure is given for recognizing sets of inference rules that generate polynomial time decidable inference relations. The procedure can automatically recognize the tractability of the inference rules underlying congruence closure. The recognition of tractability for that particular rule set constitutes mechanical verification of a theorem originally proved independently by Kozen and Shostak. The procedure is algorithmic, rather than heuristic, and the class of automatically recognizable tractable rule sets can be precisely characterized. A series of examples of rule sets whose tractability is nontrivial, yet machine recognizable, is also given. The technical framework developed here is viewed as a first step toward a general theory of tractable inference relations.

REFERENCES

• 1: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 2: ~GIVAN, R., MCALLESTER, D., AND SHALABY, S. Natural language based inference procedures ~applied to Schubert's steamroller. In Proceedings of the AAAI-91. (July). Morgan-Kaufmann, ~San Mateo, Calif., 1991, pp. 915-920.
• 3: Dexter Kozen, Complexity of finitely presented algebras, Proceedings of the ninth annual ACM symposium on Theory of computing, p.164-177, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803406]
• 4: David A. McAllester, Ontic: a knowledge representation system for mathematics, MIT Press, Cambridge, MA, 1989
• 5: David McAllester , Robert Givan, Taxonomic syntax for first order inference, Journal of the ACM (JACM), v.40 n.2, p.246-283, April 1993 [doi>10.1145/151261.151264]
• 6: ~NLAL, R. Tlle Computatiotzal Complexi_tv of Taxonomic Inference. University of Toronto, ~Toronto, Ont., Canada, Dec. 1989.
• 7: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 8: Robert E. Shostak, An algorithm for reasoning about equality, Communications of the ACM, v.21 n.7, p.583-585, July 1978 [doi>10.1145/359545.359570]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Deduction (e.g., natural, rule-based)

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic; Mechanical theorem proving

General Terms:
Algorithms, Verification

Keywords:
automated reasoning, inference rules, machine inference, mechanical verification, polynomial-time algorithm, proof systems, proof theory, theorem proving