Abstract
We present here a new technique for establishing completeness of refutational theorem proving strategies. This method employs semantic trees and, in contrast to most of the semantic tree methods, is based on proof by refutation instead of proof by induction. Thus, it works well on transfinite semantic trees as well as on finite ones. This method is particularly useful for proving the completeness of strategies with the presence of the equality predicate. We have used the method to prove the completeness of the following strategies (without the need of the functional reflexive axioms), where the precise definition of oriented paramodulation will be given later.
• Resolution + oriented paramodulation
• P1-resolution + oriented paramodulation
• Resolution with ordered predicates + oriented paramodulation using clauses only containing the equality predicate
• unfailing Knuth-Bendix-Huet algorithm
• The EN-Strategy ([Hsi85])
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
1. References
D. Brand, “Proving Theorems with the Modification Method”, SIAM J. of Computing, 4, (1975), 412–430.
C. L. Chang and C. T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
N. Dershowitz, “Orderings for Term Rewriting Systems”, J.TCS, 17, 3 (1982), 279–301.
J. Hsiang, “Two Results in Term Rewriting Theorem Proving”, Proc. of 1st International Conference in Rewrite Techniques and Applications, May, 1985.
J. P. Jouannaud, P. Lescanne and F. Reinig, “Recursive Decomposition Ordering”, Conf. on Formal Description of Programming Concepts II, 1982, 331–346.
D. E. Knuth and P. B. Bendix, “Simple Word Problems in Universal Algebras”, in Computational Algebra, J. Leach, (ed.), Pergamon Press, 1970, 263–297.
R. A. Kowalski and P. Hayes, “Semantic Trees in Automatic Theorem Proving”, in Machine Intelligence, vol. 5, B. Meltzer and D. Michie, (eds.), American Elsevier, 1969, 181–201.
D. S. Lankford and A. M. Ballantyne, “The Refutation Completeness of Blocked Permutative Narrowing and Resolution”, 4th Conf. on Automated Deduction, Austin, TX, 1979.
G. E. Peterson, “A Technique for Establishing Completeness Results in Theorem Proving with Equality”, SIAM J. of Computing, 12, 1 (1983), 82–100.
D. A. Plaisted, “A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems”, UIUCDCS-R-78-943, Univ. of Illinois, Urbana, IL, 1978.
J. A. Robinson, “A Machine Oriented Logic based on the Resolution Principle”, J. ACM, 12, 1 (January 1965), 23–41.
J. Slagle, “Automated Theorem Proving with Simplifiers, Commutativity, Associativity”, J. ACM, 21, (1974), 622–642.
L. Wos and G. A. Robinson, “Paramodulation and Set of Support”, Lecture Notes in Math. No 125, Springer-Verlag, 1970.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hsiang, J., Rusinowitch, M. (1986). A new method for establishing refutational completeness in theorem proving. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_86
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_86
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive