language: en

Taxonomic Syntax for First Order Inference

DAVID MCALLESTER and ROBERT GIVAN
Massachusetts Institute of Technology, Cambridge Massachusetts

Abstract: We identify a new polynomial time decidable fragment of first order logic and present a general method for using polynomial time inference procedures in knowledge representation systems. Our results indicate that a non-standard "taxonomic" syntax is essential in constructing natural and powerful polynomial time inference procedures. The central role of taxonomic syntax in our polynomial time inference procedures provides technical support for the often expressed intuition that knowledge is better represented in terms of taxonomic relationships than classical first order formulas. To use our procedures in a knowledge representation system we define a "Socratic proof system" which is complete for first order inference and which can be used as a semi-automated interface to a first order knowledge base.

Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical logic | computational logic, mechanical theorem proving; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving | deduction General Terms: Deduction, Algorithms Additional Keywords and Phrases: Proof Theory, Machine Inference, Theorem Proving, Automated Reasoning, Polynomial Time Algorithms, Inference Rules, Proof Systems, Mechanical Verification.

[This research was supported in part by National Science Foundation Grant IRI-8819624 and in part by the Advanced Research Projects Agency of the Department of Defense under Office of Naval Research contract N00014-85-K-0124 and N00014-89-J-3202.]

[Author's Address:]

MIT Artificial Intelligence Laboratory,
545 Technology Square, Cambridge Mass, 02139,
DAM@ai.mit.edu

[This paper appeared in JACM, vol. 40, no. 2, April 1993.]

[A postscript electronic source for this paper can be found in ftp.ai.mit.edu:/pub/dam/jacm1.ps. A bibtex reference can be found in internet file ftp.ai.mit.edu:/pub/dam/dam.bib.]