Theory reasoning in first order calculi

  • Ulrich Furbach
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 777)


Building in special theories into first order calculi is used in various applications of deduction to increase efficiency of proof procedures. We give a brief review of methods for the combination of theories with deduction or logic programming. We show how a whole family of first order calculi can be extended for theory handling; these calculi are related to each other by a simulability relation. One of these calculi is tableau model elimination which can be implemented very efficiently by Prolog Technology Theorem Proving (PTTP). A PPTP-prover which is able to handle universal theories is presented and some examples are given to show that the use of built-in theories can increase efficiency drastically.


Inference Rule Theorem Prover Horn Clause Theory Reasoning Universal Theory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AS92]
    Owen L. Astrachan and Mark E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction (CADE-11), pages 224–238. Springer-Verlag, June 1992. LNAI 607.Google Scholar
  2. [Bau92]
    P. Baumgartner. A Model Elimination Calculus with Built-in Theories. In H.-J. Ohlbach, editor, Proceedings of the 16-th German AI-Conference (GWAI-92), pages 30–42. Springer, 1992. LNAI 671.Google Scholar
  3. [Bau93a]
    P. Baumgartner. Linear Completion: Combining the Linear and the Unit-Resulting Restrictions. Research Report 9/93, University of Koblenz, 1993. (submitted).Google Scholar
  4. [Bau93b]
    P. Baumgartner. Refinements of Theory Model Elimination and a Variant without Contrapositives. Research Report 8/93, University of Koblenz, 1993.Google Scholar
  5. [BDS93]
    M. Buchheit, F.M. Donini, and A. Schaerf. Decidable reasoning in termininological knowledge representation systems. Journal of Artificial Intelligence Research, 1:109–138, 1993.Google Scholar
  6. [BF92]
    P. Baumgartner and U. Furbach. Consolution as a Framework for Comparing Calculi. Forschungsbericht 11/92, University of Koblenz, 1992. (to appear in Journal of Symbolic Computation).Google Scholar
  7. [BF93]
    P. Baumgartner and U. Furbach. Model Elimination without Contrapositives and its Application to PTTP. Fachbericht Informatik 12/93, Universität Koblenz, 1993. (submitted).Google Scholar
  8. [BFL83]
    R. Brachmann, R. Fikes, and H. Levesque. KRYPTON: a functional approach to knowledge representation. IEEE Computer, 16(10):67–73, October 1983.Google Scholar
  9. [BFP]
    Peter Baumgartner, Ulrich Furbach, and Uwe Petermann. A unified approach to theory reasoning. To appear.Google Scholar
  10. [BGL85]
    R. Brachman, V. Gilbert, and H. Levesque. An Essential Hybrid Reasoning System: Knowledge and Symbol Level Accounts of Krypton. In Proc. IJCAI, 1985.Google Scholar
  11. [CL73]
    C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.Google Scholar
  12. [Ede91]
    E. Eder. Consolution and its Relation with Resolution. In Proc. IJCAI '91, 1991.Google Scholar
  13. [FH93]
    T. Frühwirt and P. Hanschke. Terminological reasoning with constraint handling rules. Manuscript ECRC Munich, 1993.Google Scholar
  14. [Fit90]
    M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.Google Scholar
  15. [Hol90]
    B. Hollunder. Hybrid Inferences in KL-ONE-based Knowledge Representation Systems. Research Report RR-90-6, DFKI, May 1990.Google Scholar
  16. [HR91]
    Otthein Herzog and Claus-Rainer Rollinger. Text Understanding in LILOG — Integrating Computational Linguistics and Artificial Intelligence, Final Report on the IBM Germany LILOG-Project. Springer-Verlag, 1991. LNAI 546.Google Scholar
  17. [KG93]
    W. Kießling and U. Günzer. Database reasoning — a deductive framework for solving large and complex problems by means of subsumption. This volume, 1993.Google Scholar
  18. [Khe90]
    Mohammed Nadjib Khenkhar. Eine objektorientierte Darstellung von Depiktionen auf der Grundlage von Zellmatrizen. In C. Freksa and C. Habel, editors, Repräsentation und Verarbeitung räumlichen Wissens, pages 99–112. Springer-Verlag, 1990. Informatik-Fachberichte 245.Google Scholar
  19. [Llo87]
    J. Lloyd. Foundations of Logic Programming. Symbolic Computation. Springer, second, extended edition, 1987.Google Scholar
  20. [Lov91]
    D. Loveland. Near-Horn Prolog and Beyond. Journal of Automated Reasoning, 7:1–26, 1991.Google Scholar
  21. [LSBB92]
    R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performace Theorem Prover. Journal of Automated Reasoning, 8(2), 1992.Google Scholar
  22. [Mes89]
    P. Meseguer. Constraint Satisfaction Problems: An Overview. AICOM, 2(1), March 1989.Google Scholar
  23. [MM92]
    Jörg-Peter Mohren and Jürgen Müller. A geometrical approach to depicitonal representation of spatial relations. In Proc. of ECAI, 1992.Google Scholar
  24. [Pet91]
    U. Petermann. How to build in an open theory into connection calculi. submitted to J. on Computers and Artificial Intelligence, 1991.Google Scholar
  25. [Pet93]
    U. Petermann. Completeness of the pool calculus with an open built in theory. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, 3rd Kurt Gödel Colloquium '93, number 713 in Lecture Notes in Computer Science, pages 264–277. Springer-Verlag, 1993.Google Scholar
  26. [Sie89]
    Jörg H. Siekmann. Unification Theory. Journal of Symbolic Computation, 7(1):207–274, January 1989.Google Scholar
  27. [Sti85]
    M.E. Stickel. Automated Deduction by Theory Resolution. Journal of Automated Reasoning, 1:333–355, 1985.Google Scholar
  28. [Sti86]
    M. Stickel. Schubert's Steamroller Problem: Formulations and Solutions. Journal of Automated Reasoning, 2:89–101, 1986.Google Scholar
  29. [Sti88]
    M. Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4:353–380, 1988.Google Scholar
  30. [Van89]
    Pascal Van Hentenryck. Constraint Satisfaction in Logic Programming. Logic Programming. The MIT Press, Cambridge, Massachusetts, USA/London, England, UK, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Ulrich Furbach
    • 1
  1. 1.Institut für InformatikUniversität KoblenzKoblenzGermany

Personalised recommendations