Selected papers that cite this one
- Yves Andre and Francis Bossut. On the equivalence problem for letter-to-letter top-down tree transducers. Theoretical Computer Science, 205(1-2):207-229, 28 September 1998.
- Leo Bachmair and Nachum Dershowitz. Equational inference, canonical proofs, and proof orderings. Journal of the ACM, 41(2):236-276, March 1994.
- Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217-247, June 1994.
- Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation. Information and Computation, 121(2):172-192, September 1995.
- Marco Bellia and M. Eugenia Occhiuto. Suprema of open and closed formulas and their application to resolution. Information and Computation, 117(1):136-150, 15 February 1995.
- Gérard Berry and Georges Gonthier. The ESTEREL synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19(2):87-152, November 1992.
- Marc Bezem, Jan Willem Klop, and Vincent van Oostrom. Diagram techniques for confluence. Information and Computation, 141(2):172-204, 15 March 1998.
- Reinhard Bündgen. Buchberger's algorithm: The term rewriter's point of view. Theoretical Computer Science, 159(2):143-190, 3 June 1996. Fundamental Study.
- David Clark and Richard Kennaway. Event structures and non-orthogonal term graph rewriting. Mathematical Structures in Computer Science, 6(6):545-578, December 1996.
- Thierry Coquand. An analysis of Ramsey's theorem. Information and Computation, 110(2):297-304, 1 May 1994.
- Bruno Courcelle and Paul Franchi-Zannettacci. On the equivalence problem for attribute systems. Information and Control, 52(3):275-305, March 1982.
- Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362-397, March 1996.
- G. Dányi and Z. Fülöp. Compositions with superlinear deterministic top-down tree transformations. Theoretical Computer Science, 194(1-2):57-85, 10 March 1998.
- Jörg Denzinger and Stephan Schulz. Automatic acquisition of search control knowledge from multiple proof attempts. Accepted for publication in Information and Computation. Final manuscript received for publication October 2, 1998.
- Henk Doornbos, Roland Backhouse, and Jaap van der Woude. A calculational approach to mathematical induction. Theoretical Computer Science, 179(1-2):103-135, 1 June 1997. Fundamental Study.
- Daniel J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101(2):251-267, December 1992.
- Daniel J. Dougherty and Ramesh Subrahmanyam. Equality between functionals in the presence of coproducts. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 282-291, San Diego, California, 26-29 June 1995. IEEE Computer Society Press.
- Jean Gallier, Paliath Narendran, David Plaisted, Stan Raatz, and Wayne Snyder. An algorithm for finding canonical sets of ground rewrite rules in polynomial time. Journal of the ACM, 40(1):1-16, January 1993.
- Jean Gallier, Paliath Narendran, Stan Raatz, and Wayne Snyder. Theorem proving using equational matings and rigid E-unification. Journal of the ACM, 39(2):377-429, April 1992.
- Pál Gyenizse and Sándor Vágvölgyi. Linear generalized semi-monadic rewrite systems effectively preserve recognizability. Theoretical Computer Science, 194(1-2):87-122, 10 March 1998.
- Fritz Henglein. Dynamic typing: syntax and proof theory. Science of Computer Programming, 22(3):197-230, June 1994.
- Jieh Hsiang and Michaël Rusinowitch. Proving refutational completeness of theorem-proving strategies: The transfinite semantic tree method. Journal of the ACM, 38(3):559-587, July 1991.
- Masahito Kurihara and Azuma Ohuchi. Modularity in noncopying term rewriting. Theoretical Computer Science, 152(1):139-169, 11 December 1995.
- Yves Lafont and Alain Prouté Church-Rosser property and homology of monoids. Mathematical Structures in Computer Science, 1(3):297-326, November 1991.
- Björn Lisper. Total unfolding: theory and applications. Journal of Functional Programming, 4(4):479-498, October 1994.
- Björn Lisper. Computing in unpredictable environments: semantics, reduction strategies, and program transformations. Theoretical Computer Science, 190(1):61-85, 10 January 1998.
- Klaus Madlener and Birgit Reinert. Relating rewriting techniques on monoids and rings: congruences on monoids and ideals in monoid rings. Theoretical Computer Science, 208(1-2):3-31, 28 November 1998.
- Kim Marriott and Martin Odersky. A confluent calculus for concurrent constraint programming. Theoretical Computer Science, 173(1):209-233, 20 February 1997.
- Yuri Matiyasevich and Géraud Sénizergues. Decision problems for semi-Thue systems with a few rules. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 523-531, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.
- Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3-29, 10 February 1998.
- José Meseguer and Joseph A. Goguen. Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems. Information and Computation, 103(1):114-158, March 1993.
- N. Lafaye de Micheaux and C. Rambaud. Confluence for graph transformations. Theoretical Computer Science, 154(2):329-348, 5 February 1996.
- Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms. A generalization of environments. Theoretical Computer Science, 198(1-2):49-98, 30 May 1998. Fundamental Study.
- Joachim Niehren. Functional computation as concurrent computation. In Conference Record of POPL '96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 333-343, St. Petersburg Beach, Florida, 21-24 January 1996.
- Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 30 March 1997.
- F. Otto. On confluence versus strong confluence for one-rule trace-rewriting systems. Mathematical Systems Theory, 28(4):363-384, July/August 1995.
- Masahiko Sakai and Yoshihito Toyama. Semantics and strong sequentiality of priority term rewriting systems. Theoretical Computer Science, 208(1-2):87-110, 28 November 1998.
- Géraud Sénizergues. A polynomial algorithm testing partial confluence of basic semi-Thue systems. Theoretical Computer Science, 192(1):55-75, 10 February 1998.
- Y. Toyama, Jan Willem Klop, and H. P. Barendregt. Termination for direct sums of left-linear complete term rewriting systems. Journal of the ACM, 42(6):1275-1304, November 1995.
- Ralf Treinen. The first-order theory of linear one-step rewriting is undecidable. Theoretical Computer Science, 208(1-2):179-190, 28 November 1998.
- Rakesh M. Verma. A theory of using history for equational systems with applications. Journal of the ACM, 42(5):984-1020, September 1995.
- Tie-Cheng Wang. Z-module reasoning: An equality-oriented proving method with built-in ring axioms. Journal of the ACM, 40(3):558-606, July 1993.
- C. Wrathall and V. Diekert. On confluence of one-rule trace-rewriting systems. Mathematical Systems Theory, 28(4):341-361, July/August 1995.