Thumbnail
Access Restriction
Subscribed

Author McAllester, David ♦ Givan, Robert
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1993
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Automated reasoning ♦ Inference rules ♦ Machine inference ♦ Mechanical verification ♦ Polynomial time algorithms ♦ Proof systems ♦ Proof theory ♦ Theorem proving
Abstract A new polynomial time decidable fragment of first order logic is identified, and a general method for using polynomial time inference procedures in knowledge representation systems is presented. The results shown in this paper indicate that a nonstandard “taxonomic” syntax is essential in constructing natural and powerful polynomial time inference procedures. The central role of taxonomic syntax in the 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 the procedures in a knowledge representation system, a “Socratic proof system” is defined, which is complete for first order inference and which can be used as a semi-automated interface to a first order knowledge base.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1993-04-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 40
Issue Number 2
Page Count 38
Starting Page 246
Ending Page 283


Open content in new tab

   Open content in new tab
Source: ACM Digital Library