Abstract
In this paper we present an ordered theory resolution calculus and prove its completeness. Theory reasoning means to relieve a calculus from explicitly drawing inferences in a given theory by special purpose inference rules (e.g. E-resolution for equality reasoning). We take advantage of orderings (e.g. simplification orderings) by disallowing to resolve upon clauses which violate certain maximality constraints; stated positively, a resolvent may only be built if all the selected literals are maximal in their clauses. By this technique the search space is drastically pruned. As an instantiation for theory reasoning we show that equality can be built in by rigid E-unification.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Anderson and W. Bledsoe. A linear fonnat for resolution with merging and a new technique for establishing completeness. J. of the ACM, 17:525–534, 1970.
P. Andrews. Theorem Proving via General Matings. J. ACM, 28(2):193–214, 1981.
P. Baumgartner. A Model Elimination Calculus with Built-in Theories. Fachbericht Informatik 7/91, Universität Koblenz, 1991.
R. Brachmann, R. Fikes, and H. Levesque. KRYPTON: a functional approach to knowledge representation. IEEE Computer, 16(10):67–73, October 1983.
L. Bachmair and H. Ganzinger. Completion of First-Order Clauses with Equality by Strict Superposition. In Proc. Second Int. Workshop on Conditional and Typed Rewrite Systems, LNCS. Springer, 1990.
C. Chang and R. Lee. Symbolic Logic and Mechanical TheoremProving. Academic Press, 1973.
Nachum Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 3(1&2):69–116, February/April 1987.
J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-Completeness and Applications to Equational Matings. Information and Computation, pages 129–195, 1990.
J. Hsiang and M. Rusinowitch. A New Method for Establishing Refutational Completeness in Theorem Proving. In Proc. 8th CADE, pages 141–152. Springer, 1986.
N. Murray and E. Rosenthal. Theory Links: Applications to Automated Theorem Proving. J. of Symbolic Computation, 4:173–190, 1987.
H. J. Ohlbach and J. Siekmann. The Markgraf Karl Refutation Procedure. In J.L. Lassez and G. Plotkin, editors, Computational Logic— Essays in Honor of Alan Robinson, pages 41–112. MIT Press, 1991.
U. Petermann. Towards a connection procedure with built in theories. In JELIA 90. European Workshop on Logic in AI, Springer, LNCS, 1990.
J.A. Robinson. A machine-oriented logic based on the resolution principle. JACM, 12(1):23–41, January 1965.
M.E. Stickel. Theory Resolution: Building in Nonequational Theories. SRI International Research Report Technical Note 286, Artificial Intelligence Center, 1983.
M.E. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, pages 333–356, 1985.
H. Zhang and D. Kapur. First-Order Theorem Proving Using Conditional Rewrite Rules. In E. Lusk and R. Overbeek, editors, Lecture Notes in Computer Science: 9th International Conference on Automated Deduction, pages 1–20. Springer-Verlag, May 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baumgartner, P. (1992). An ordered theory resolution calculus. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1992. Lecture Notes in Computer Science, vol 624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013054
Download citation
DOI: https://doi.org/10.1007/BFb0013054
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55727-2
Online ISBN: 978-3-540-47279-7
eBook Packages: Springer Book Archive