Abstract
The paper presents a new system of inference rules for the completion of conditional equations. Conditional equations that are generated during completion can either be eliminated, oriented into reductive rewrite rules or considered as nonoperational. Rewrite rules are, as usual, subject to critical pair computation. Nonoperational equations are superposed by the rewrite rules on one of their conditions. A conditional equation can be eliminated if there is also a proof of the equation which is simpler than the equation itself. The purpose of this paper is to present a technique in which the origin of an equation defines the complexity bound which alternative proofs must respect. This technique is shown to be particularly useful in the conditional case, making the completion process terminate on a number of nontrivial specifications which it would fail to terminate otherwise.
This work is partially supported by the ESPRIT-project PROSPECTRA, ref≠390.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
7 References
Bachmair, L.: Proof methods for equational theories. PhD-Thesis, U. of Illinois, Urbana Champaign, 1987.
Bachmair, L. and Dershowitz, N.: Critical pair criteria for the Knuth-Bendix completion procedure. Proc. ACM Symp. on Symbolic and Alg. Computation, 1986, 215–217.
Bachmair, L., Dershowitz, N. and Hsiang, J.: Proof orderings for equational proofs. Proc. LICS 86, 346–357.
Bertling, H., Ganzinger, H. and Schäfers, R.: CEC: A system for conditional equational completion. User Manual Version 1.0, PROSPECTRA-Report M.1.3-R-7.0, U. Dortmund, 1988.
Dershowitz, N.: Termination. Proc. RTA 1985, LNCS 202, 1985, 180–224.
Dershowitz, N. and Manna, Z.: Proving termination with multiset orderings. CACM 22 (1979), 465–476.
Ganzinger, H.: A Completion procedure for conditional equations. Report 234, U. Dortmund, 1987 (revised version to appear in J. Symb. Computation).
Huet, G. and Oppen, D.C.: Equations and Rewrite Rules. A Survey. In: R. Book (ed): Formal Languages: Perspectives and open Problems. Academic Press, New York, 1980, 349–405.
Jouannaud, J.P. and Waldmann, B.: Reductive conditional term rewriting systems. Proc. 3rd TC2 Working Conference on the Formal Description of Prog. Concepts, Ebberup, Denmark, Aug. 1986, North-Holland.
Kaplan, St.: Conditional rewrite rules. TCS 33 (1984), 175–193.
Kaplan, St.: Fair conditional term rewrite systems: unification, termination and confluence. Report 194, U. de Paris-Sud, Centre d'Orsay, Nov. 1984.
Kaplan, St. and Remy J.-L.: Completion algorithms for conditional rewriting systems. MCC Workshop on Resolution of Equations in Algebraic Structures, Austin, May 1987.
Kirchner, C, Kirchner, H., and Meseguer, J.: Operational semantics of OBJ3. Proc. ICALP 88, 1988, to appear.
Kapur, D., Narendran, P., and Sivakumar, G.: A path ordering for proving termination of term rewrite systems. LNCS 186, 1985, 173–187.
Kounalis, E. and Rusinowitch, M.: On word problems in Horn logic. Proc. 1st Int'l Workshop on Conditional Term Rewriting, Orsay, 1987, to appear in LNCS.
Küchlin, W.: A confluence criterion based on the generalised Newman lemma. Proc. Eurocal 1985, LNCS 204, 1985, 390–399.
Küchlin, W.: Equational completion by proof transformation. Ph.D. thesis, Dep't. of Mathematics, ETH Zürich, 1986.
Réty, P.: Méthodes d'unification par surréduction. Thesis, U. de Nancy 1, 1988.
Rusinowitch, M.: Theorem-proving with resolution and superposition: an extension of Knuth and Bendix procedure as a complete set of inference rules. Report 87-R-128, CRIN, Nancy, 1987.
Smolka, G., Nutt, W., Goguen, J.A. and Meseguer, J.: Order-sorted equational computation. SEKI Report SR-87-14, U. Kaiserslautern, 1987.
Winkler, F. and Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. Coll. on Algebra, Combinatorics and Logic in Comp. Sci., Györ, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganzinger, H. (1988). Completion with history-dependent complexities for generated equations. In: Sannella, D., Tarlecki, A. (eds) Recent Trends in Data Type Specification. ADT 1987. Lecture Notes in Computer Science, vol 332. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50325-0_4
Download citation
DOI: https://doi.org/10.1007/3-540-50325-0_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50325-5
Online ISBN: 978-3-540-45970-5
eBook Packages: Springer Book Archive