Taxonomic syntax for first order inference

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.

REFERENCES

• 1: ~BELL, J., AND MACHOVER, M. A Course m MathematzcalLogic. North-Holland, Amsterdam, ~The Netherlands, 1977.
• 2: ~BOYER, R. S., BLEDSOE, W. W., AND HENNEMAN, W.H. Computer proofs of hmit theorems. ~ArtiX. bzt. 3 (1972), 27-60.
• 3: ~BOYER, R. S., AND MOORE, J.S. A ComputationalLogic. ACM Monograph Series Academic ~Press, New York, 1979.
• 4: ~BRACHMAN, R., AND SCHMOLZE, J. An overview of the kl-one knowledge representation ~system. Comput. Int. 9, 2 (1985), 171-216.
• 5: J. M. Crawford , Benjamin Kuipers, Towards a theory of access-limited logic for knowledge representation, Proceedings of the first international conference on Principles of knowledge representation and reasoning, p.67-78, December 1989
• 6: ~DAVIS, M. Obvious logical inferences. In Proceedings ofA,4AI-81. Morgan-Kaufmann, San ~Mateo, Calif., 1981, pp. 530-531.
• 7: ~DONINI, F.~ LENZERINI, m., NARDI, D., AND NUTT, W. The complexity of concept languages. ~In Proceeding* ofKR91. Morgan-Kaufmann, San Mateo, Cahf., 1991, pp. 151-162.
• 8: 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]
• 9: ~DOWNING, W., AND GALLIER, J. H. Linear time algorithms for testing the sansfiabdity of ~propositional horn formulae. J. Logic Prog. 1, 3 (1984), 267-284.
• 10: Deepak Kapur , G. Sivakumar , Hantao Zhang, RRL: A Rewrite Rule Laboratory, Proceedings of the 8th International Conference on Automated Deduction, p.691-692, July 27-August 01, 1986
• 11: Jussi Ketonen, EKL—a mathematically oriented proof checker, Proc. of the conference on 7th international conference on automated deduction, p.65-79, September 1984, Napa, California, United States
• 12: Kurt Konolige, A Deduction Model of Belief, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1986
• 13: 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]
• 14: David A. McAllester, Ontic: a knowledge representation system for mathematics, MIT Press, Cambridge, MA, 1989
• 15: David A. McAllester, Automatic recognition of tractability in inference relations, Journal of the ACM (JACM), v.40 n.2, p.284-303, April 1993 [doi>10.1145/151261.151265]
• 16: B. Nebel, Terminological reasoning is inherently intractable (research note), Artificial Intelligence, v.43 n.2, p.235-249, May 1990 [doi>10.1016/0004-3702(90)90087-G]
• 17: 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]
• 18: ~PARK, D. Finiteness is /~-ineffable. Theoret. Comput. Sci. 3, 2 (1976), 173-181.
• 19: Judea Pearl, Probabilistic reasoning in intelligent systems: networks of plausible inference, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 20: V. R. Pratt, On specifying verifiers, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-116, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567457]
• 21: Manfred Schmidt-Schaubß , Gert Smolka, Attributive concept descriptions with complements, Artificial Intelligence, v.48 n.1, p.1-26, Feb. 1991 [doi>10.1016/0004-3702(91)90078-X]
• 22: Christoph Walther, Many-sorted unification, Journal of the ACM (JACM), v.35 n.1, p.1-17, Jan. 1988 [doi>10.1145/42267.45071]

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.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.0 General
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving; Computational logic

General Terms:
Algorithms, Verification

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