Abstract
We present an approach to building-in equational reasoning into theorem provers which are based on the connection method. The approach is an instance of total theory reasoning. In order to achieve a completeness result we combine results concerning the simultaneous rigid E-unification problem with our general framework for building-in theories. We pose the problem whether for the construction of a complete goal-oriented prover with equality it is sufficient to be able to solve only a restricted version of the simultaneous rigid E-unification problem.
This research has been supported by grants of the Deutsche Forschungsgemeinschaft and the Alexander von Humboldt-Stiftung.
Preview
Unable to display preview. Download preview PDF.
References
P. Andrews. Theorem Proving via General Matings. J. ACM, 28(2):193–214, 1981.
G. Becher and U. Petermann. Rigid E-Unification by Completion and Rigid Paramodulation (Extended version). Technical report, Dec. 1993. Les Cahiers du L.A.I.A.C. University of Caen. 1993.
B. Beckert. Ein vervollständigungsbasiertes Verfahren rar Behandlung von Gleichheit im Tableaukalkül mit freien Variablen. Master's thesis, Universität Karlsruhe (TH), 1993.
B. Beckert and R. Hähnle. An improved method for adding equality to free variable semantic tableaux. In D. Kapur, editor, Proceedings, 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY, LNCS 607, pages 507–521. Springer, 1992.
W. Bibel. Automated Theorem Proving. Vieweg, 1st edition, 1982.
W. Bibel, S. Brüning, U. Egly, and T. Rath. KoMeT. In W. Bibel, editor, DFG-Kolloquium Schwerpunktprogramm “Deduktion”, pages 19–20. TH Darmstadt, 1994.
D. Brand. Proving theorems with the modification method. SIAM Journal of Computation, 4:412–430, 1975.
J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Theorem Proving with Equational Matings and Rigid E-unification. J. of ACM, 1992.
J. Goubault. A Rule-Based Algorithm for Rigid E-Unification. In G. Gottlob, A. Leitsch, and D. Mundici, editors, 3rd Kurt Gödel Colloquium '93, volume 713 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performace Theorem Prover. Journal of Automated Reasoning, 8:183–212, 1992.
D. Loveland. Automated Theorem Proving — A Logical Basis. North Holland, 1978.
D. W. Loveland. Mechanical Theorem Proving by Model Elimination. JACM, 15(2), 1978.
M. Moser. Improving transformation systems for general e-unification. In RTA '93: Rewriting Techniques and Applications, number 690 in LNCS, pages 92–105. Springer, 1993.
G. Neugebauer and U. Petermann. CaPrl: Integrating theories into the prolog technology theorem prover ProCom. In CADE '94t Workshop on Theory Reasoning, 1994. to appear.
G. Neugebauer and T. Schaub. A pool-based connection calculus. Technical Report AIDA-91-02, FG Intellektik, Technische Hochschule Darmstadt, 1991.
U. Petermann. Completeness of the pool calculus with an open built in theory. NTZ-Report 24/93, Naturwissenschaftlich-Theoretisches Zentrum der Universität Leipzig, 1993.
U. Petermann. Completeness of the pool calculus with an open built in theory. In G. Gottlob, A. Leitsch, and D. Mundici, editors, 3rd Kurt Gödel Colloquium '93, volume 713 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
H. Reichel. Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford University Press, Oxford, 1987.
W. Snyder and C. Lynch. Goal directed strategies for paramodulation. In R. Book, editor, Rewriting Techniques and Applications, Lecture Notes in Computer Science No. 488, pages 150–161, Berlin, 1991. Springer.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Petermann, U. (1994). A complete connection calculus with rigid E-unification. In: MacNish, C., Pearce, D., Pereira, L.M. (eds) Logics in Artificial Intelligence. JELIA 1994. Lecture Notes in Computer Science, vol 838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021970
Download citation
DOI: https://doi.org/10.1007/BFb0021970
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58332-5
Online ISBN: 978-3-540-48657-2
eBook Packages: Springer Book Archive