Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
P. Baumgartner. Linear Completion: Combining the Linear and the Unit-Resulting Restrictions. Research Report 9/93, University of Koblenz, 1993. (submitted).
P. Baumgartner. Refinements of Theory Model Elimination and a Variant without Contrapositives. Research Report 8/93, University of Koblenz, 1993.
M. Buchheit, F.M. Donini, and A. Schaerf. Decidable reasoning in termininological knowledge representation systems. Journal of Artificial Intelligence Research, 1:109–138, 1993.
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).
P. Baumgartner and U. Furbach. Model Elimination without Contrapositives and its Application to PTTP. Fachbericht Informatik 12/93, Universität Koblenz, 1993. (submitted).
R. Brachmann, R. Fikes, and H. Levesque. KRYPTON: a functional approach to knowledge representation. IEEE Computer, 16(10):67–73, October 1983.
Peter Baumgartner, Ulrich Furbach, and Uwe Petermann. A unified approach to theory reasoning. To appear.
R. Brachman, V. Gilbert, and H. Levesque. An Essential Hybrid Reasoning System: Knowledge and Symbol Level Accounts of Krypton. In Proc. IJCAI, 1985.
C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
E. Eder. Consolution and its Relation with Resolution. In Proc. IJCAI '91, 1991.
T. Frühwirt and P. Hanschke. Terminological reasoning with constraint handling rules. Manuscript ECRC Munich, 1993.
M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.
B. Hollunder. Hybrid Inferences in KL-ONE-based Knowledge Representation Systems. Research Report RR-90-6, DFKI, May 1990.
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.
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.
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.
J. Lloyd. Foundations of Logic Programming. Symbolic Computation. Springer, second, extended edition, 1987.
D. Loveland. Near-Horn Prolog and Beyond. Journal of Automated Reasoning, 7:1–26, 1991.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performace Theorem Prover. Journal of Automated Reasoning, 8(2), 1992.
P. Meseguer. Constraint Satisfaction Problems: An Overview. AICOM, 2(1), March 1989.
Jörg-Peter Mohren and Jürgen Müller. A geometrical approach to depicitonal representation of spatial relations. In Proc. of ECAI, 1992.
U. Petermann. How to build in an open theory into connection calculi. submitted to J. on Computers and Artificial Intelligence, 1991.
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.
Jörg H. Siekmann. Unification Theory. Journal of Symbolic Computation, 7(1):207–274, January 1989.
M.E. Stickel. Automated Deduction by Theory Resolution. Journal of Automated Reasoning, 1:333–355, 1985.
M. Stickel. Schubert's Steamroller Problem: Formulations and Solutions. Journal of Automated Reasoning, 2:89–101, 1986.
M. Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4:353–380, 1988.
Pascal Van Hentenryck. Constraint Satisfaction in Logic Programming. Logic Programming. The MIT Press, Cambridge, Massachusetts, USA/London, England, UK, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Furbach, U. (1994). Theory reasoning in first order calculi. In: von Luck, K., Marburger, H. (eds) Management and Processing of Complex Data Structures. IS/KI 1994. Lecture Notes in Computer Science, vol 777. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57802-1_8
Download citation
DOI: https://doi.org/10.1007/3-540-57802-1_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57802-4
Online ISBN: 978-3-540-48335-9
eBook Packages: Springer Book Archive