Abstract
We have previously shown that strict superposition together with merging paramodulation is refutationally complete for first-order clauses with equality. This paper improves these results by considering a more powerful framework for simplification and elimination of clauses. The framework gives general criteria under which simplification and elimination do not destroy the refutation completeness of the superposition calculus. One application is a proof of the refutation completeness for alternative superposition strategies with arbitrary selection functions for negative literals. With these powerful simplification mechanisms it is often possible to compute the closure of nontrivial sets of clauses under superposition in a finite number of steps. Refutation or solving of goals for such closed or complete sets of clauses is simpler than for arbitrary sets of clauses. The results in this paper contain as special cases or generalize many known results about about ordered Knuth-Bendix-like completion of equations, of Horn clauses, of Horn clauses over built-in Booleans, about completion of first-order clauses by clausal rewriting, and inductive theorem proving for Horn clauses.
Extended Abstract
The research described in this paper was supported in part by the National Science Foundation under grant CCR-8901322, by the ESPRIT project PROSPECTRA (ref. no. 390), and by a travel grant from Deutsche Forschungsgemeinschaft.
A full version of this paper containing all the proofs of the theorems is available as Research Report No. 372, FB Informatik, Universität Dortmund, 1990.
Part of this work was done while the second author was on leave at SUNY at Stony Brook.
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
References
L. Bachmair, N. Dershowitz, and D. Plaisted, 1989. Completion without failure. In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, vol. 2, pp. 1–30. Academic Press.
H. Bertling and H. Ganzinger, 1989. Completion-time optimization of rewrite-time goal solving. In Proc. 3rd Int Conf. Rewriting Techniques and Applications, Lect. Notes in Comput. Sci., vol. 355, Berlin, Springer-Verlag.
L. Bachmair and H. Ganzinger, 1990. On restrictions of ordered paramodulation with simplification. In Proc. 10th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 449, pp. 427–441, Berlin, Springer-Verlag.
L. Bachmair and H. Ganzinger, 1991. Perfect Model Semantics for Logic Programs with Equality. Submitted for publication.
N. Dershowitz, 1991. A Maximal-Literal Unit Strategy for Horn Clauses. In Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, Lect. Notes in Comput. Sci., vol. to appear, Berlin, Springer-Verlag.
H. Ganzinger, 1987. A completion procedure for conditional equations. In S. Kaplan and J.-P. Jouannaud, editors, Conditional Term Rewriting Systems, Lect. Notes in Comput. Sci., vol. 308, pp. 62–83, Berlin, Springer-Verlag. To appear in J. Symbolic Computation.
H. Ganzinger, 1987. Ground term confluence in parametric conditional equational sepcifications. In STACS'87, Lect. Notes in Comput. Sci., vol. 247, pp. 286–298, Berlin, Springer-Verlag.
J. Hsiang and M. Rusinowitch, 1987. On word problems in equational theories. In T. Ottmann, editor, Proc. 14th ICALP, Lect. Notes in Comput. Sci., vol. 267, pp. 54–71, Berlin, Springer-Verlag.
J. Hsiang and M. Rusinowitch, 1989. Proving refutational completeness of theorem proving strategies: The transfinite semantic Tree method. Submitted for publication, 1989.
D. Knuth and P. Bendix, 1970. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford.
E. Kounalis and M. Rusinowitch, 1988. On word problems in Horn theories. In E. Lusk and R. Overbeek, editors, Proc. 9th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 310, pp. 527–537, Berlin, Springer-Verlag.
D. Lankford, 1975. Canonical inference. Technical Report ATP-32, Dept. of Mathematics and Computer Science, University of Texas, Austin.
U. Martin and T. Nipkow, 1989. Ordered Rewriting and Confluence. Technical Report, Univ. of Cambridge, Cambridge, U.K.
R. Nieuwenhuis and F. Orejas, 1991. Clausal Rewriting. In Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, Lect. Notes in Comput. Sci., vol. to appear, Berlin, Springer-Verlag.
M. Rusinowitch, 1988. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix procedure as a complete set of inference rules. Submitted for publication, 1988.
G.A. Robinson and L. T. Wos, 1969. Paramodulation and theorem proving in first order theories with equality. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pp. 133–150. American Elsevier, New York.
L. T. Wos, G. A. Robinson, D. F. Carson, and L. Shalla, 1967. The concept of demodulation in theorem proving. Journal of the ACM, Vol. 14, pp. 698–709.
H.T. Zhang and J-L. Rémy, 1985. Contextual Rewriting. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, Lect. Notes in Comput. Sci., vol. 202, pp. 46–62, Berlin, Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bachmair, L., Ganzinger, H. (1991). Completion of first-order clauses with equality by strict superposition. In: Kaplan, S., Okada, M. (eds) Conditional and Typed Rewriting Systems. CTRS 1990. Lecture Notes in Computer Science, vol 516. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54317-1_89
Download citation
DOI: https://doi.org/10.1007/3-540-54317-1_89
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54317-6
Online ISBN: 978-3-540-47558-3
eBook Packages: Springer Book Archive