Abstract
Superposition or critical pair computation is one of the key operations in the Knuth-Bendix completion procedure and its extensions. We propose a practical technique which can save computation of some critical pairs where the most general unifiers used to generate these critical pairs are less general than the most general unifiers used to generate other joinable critical pairs. Consequently, there is no need to superpose identical subterms at different positions in a rule more than once and there is also no need to superpose symmetric subterms in a rule more than once. The combination of this technique with other critical pair criteria proposed in the literature is also discussed. The technique has been integrated in the completion procedures for ordinary term rewriting systems as well as term rewriting systems with associative-commutative operators implemented in RRL, Rewrite Rule Laboratory. Performance of the completion procedures with and without this technique is compared on a number of examples.
Part of the work was done while the first author was at Rensselaer Polytechnic Institute, New York and was partially supported by the National Science Foundation Grant no. CCR-8408461.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Dershowitz, N. and Hsiang, J. (1986) Orderings for equational proofs. Proc. IEEE Symp. Logic in Computer Science, Cambridge, Massachusetts, pp. 346–357.
Bachmair, L., and Dershowitz, N. (1986) Critical pair criteria for the Knuth-Bendix completion procedure. Proc. of SYMSAC. See also J. of Symbolic Computation, (1988) 6, 1–18.
Bachmair, L., and Dershowitz, N. (1987) Critical pair criteria for rewriting modulo a congruence, In Proc. Eurocal 87, Leipzig, GDR.
Bledsoe, W., (1977) “Non-resolution theorem proving”, Artificial Intelligence 9, 1, pp.1–35.
Buchberger, B. (1979) A criterion for detecting unnecessary reductions in the construction of Gröbner Bases. Proc, of EUROSAM 79, Springer Verlag, LICS 72, 3–21.
Bürckert, H.-J., Herold, A., Kapur, D., Siekmann, J.H., Stickel, M., Tepp, M., and Zhang, H., (1988) Opening the AC-Unification Race, J. of Automated Reasoning, 4, 465–474.
Dershowitz, N., (1983) Applications of the Knuth-Bendix Completion Procedure. Laboratory Operation, Aerosapce Corporation, Aerospace Report No. ATR-83(8478)-2, 15.
Dershowitz, N. and Jouannaud J.P. (1988). Rewriting Systems, Handbook of Theoretical Computer Science.
Huet, G. (1980) Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM, 27/4, 797–821.
Kapur, D., Musser, D.R., and Narendran, P. (1984). Only prime superpositions need be considered for the Knuth-Bendix completion procedure. GE Corporate Research and Development Report, Schenectady. Also in J. of Symbolic Computation (1988) 4, 19–36.
Kapur, D. and Sivakumar, G. (1984). Architecture of and experiments with RRL, a Rewrite Rule Laboratory. Proceedings of an NSF Workshop on the Rewrite Rule Laboratory Sept. 6–9 Sept. 1983, General Electric Research and Development Center Report 84GEN008.
Kapur, D., Sivakumar, G., and Zhang, H. (1986). RRL: A Rewrite Rule Laboratory. Eighth International Conference on Automated Deduction (CADE-8), Oxford, England, July 1986, LNCS 230, Springer Verlag, 692–693.
Kapur, D., and Zhang, H. (1987). RRL: A Rewrite Rule Laboratory — User's Manual. GE Corporate Research and Development Report, Schenectady, NY.
Kapur, D., and Zhang, H. (1988). RRL: A Rewrite Rule Laboratory. Proc. of Ninth International Conference on Automated Deduction (CADE-9), Argonne, IL.
Knuth, D.E. and Bendix, P.B. (1970). Simple word problems in universal algebras. In: Computational Problems in Abstract Algebras. (ed. J. Leech), Pergamon Press, 263–297.
Küchlin, W. (1985). A confluence criterion based on the generalized Newman Lemma. In: EUROCAL'85 (ed. Caviness) 2, Lecture Notes in Computer Science, 204, Springer Verlag, 390–399.
Lankford, D.S., and Ballantyne, A.M. (1977). Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions. Automatic Theorem Proving Project, Dept. of Math. and Computer Science, University of Texas, Austin, Texas, Report ATP-39.
Lankford, D.S., and Ballantyne, A.M. (1979). The refutational completeness of blocked permutative narrowing and resolution. Proc. 4th Conf. on Automated Deduction, Austin, Texas.
Lusk E., and Overbeek, R., (1985) “Reasoning about equality”, Journal of Automated Reasoning 6, pp.209–228.
Peterson, G.L., and Stickel, M.E. (1981). Complete sets of reductions for some equational theories. J. ACM, 28/2, 233–264.
Slagle, J. (1974) Automated theorem proving for theories with simplifiers, commutativity and associativity. J. ACM, 4, 622–642.
Stickel, M. (1981). A complete unification algorithm for associative-commutative functions. J. ACM, 28, 3, 423–434.
Stickel, M. (1984). A case study of theorem proving by the Knuth-Bendix method: Discovering that x 3=x implies ring commutativity. Proc. of 7th Conf. on Automated Deduction, NAPA, Calif., LNCS 170, Springer Verlag, 248–258.
Veroff, R.L. (1981). Canonicalization and demodulation. Report ANL-81-6, Argonne National Lab., Argonne, IL.
Wang, T.C. (1988). Case studies of Z-module reasoning: Proving benchmark theorems for ring theory. J. of Automated Reasoning, 3.
Winkler, F. (1984). The Church-Rosser property in computer algebra and special theorem proving: an investigation of critical pair, completion algorithms”. Dissertation der J. Kepler-Universitaet, Linz, Austria.
Winkler, F., (1985) Reducing the complexity of the Knuth-Bendix completion algorithm: a ‘unification’ of different approaches. In: EUROCAL'85 (ed. Caviness) 2, Lecture Notes in Computer Science, 204, Springer Verlag, 378–389.
Winkler, F., and Buchberger, B. (1983). A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In: Proc. of the Coll. on Algebra, Combinatorics and Logic in Computer Science, Györ, Hungry.
Wos, L. (1988). Automated Reasoning: 33 basic research problems. Prentice Hall, NJ.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, H., Kapur, D. (1989). Consider only general superpositions in completion procedures. In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_129
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_129
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51081-9
Online ISBN: 978-3-540-46149-4
eBook Packages: Springer Book Archive