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 non- trival, yet machine recognizable, is also given. The technical framework developed here is reviewed as a first step toward a general theory of tractable inference relations. Keywords: Statistical inference, Machine inference, Theorem proving, Automated reasoning, Polynomial time decidability, Inference rules, Proof systems, Mechanical verification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 1990
- Accession Number
- ADA223698
Entities
People
- David Mcallester
Organizations
- Massachusetts Institute of Technology