| [aaa93] | Proceedings of the eleventh national conference on artificial intelligence, number 11, Washington, DC, 1993. |
| [Abr94] | Samson Abramsky, editor. Ninth Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE. |
| [ACL86] | 24th Annual Meeting of the Association for Computational Lingustics, New York, NY, 1986. |
| [ACL87] | 25th Annual Meeting of the Association for Computational Lingustics, 1987. |
| [Adi09] | Sergei Adian. Upper bound on the derivational complexity in some word rewriting system. Doklady Mathematics, 80(2):679-683, October 2009. [ DOI | http ] |
| [AG00] | Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133-178, 2000. |
| [AKW93] | A. Aiken, D. Kozen, and E. Wimmers. Decidability of systems of set constraints with negative constraints. Technical Report 93-1362, Computer Science Department, Cornell University, 1993. |
| [alp97] | 6th International Conference on Algebraic and Logic Programming, volume 1298 of Lecture Notes in Computer Science. Springer-Verlag, 1997. |
| [AM96] | Sergio Antoy and Aart Middeldorp. A sequential reduction strategy. Theoretical Computer Science, 165(1):75-95, 1996. |
| [AMA91] | Javier Leach Albert, Burkhard Monien, and M. Rodriguez Artalejo, editors. 18th International Colloquium on Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science, Madrid, Spain, 1991. Springer-Verlag. |
| [Aot01] | Takahito Aoto. Solution to the problem of Zantema on a persistent property of term rewriting systems. Journal of Functional and Logic Programming, 2001(11), December 2001. |
| [Apt92] | Krzysztof Apt, editor. Proceedings of the Joint International Conference and Symposium on Logic Programming, Washington, USA, November 1992. The MIT Press. |
| [AS94] | Serge Abiteboul and Eli Shamir, editors. 21th International Colloquium on Automata, Languages and Programming, volume 820 of Lecture Notes in Computer Science, Jerusalem, Israel, July 1994. Springer-Verlag. |
| [AW92] | A. Aiken and E. Wimmers. Solving systems of set constraints. In Scedrov [Sce92], pages 329-340. |
| [Baa90] | Franz Baader. Rewrite systems for varieties of semigroups. In M. Stickel, editor, Proceedings of the Tenth International Conference on Automated Deduction (Kaiserslautern, West Germany), volume 449 of Lecture Notes in Computer Science, pages 381-395, Berlin, July 1990. Springer-Verlag. |
| [Bac00] | Leo Bachmair, editor. Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, Norwich, UK, July 2000. Springer-Verlag. |
| [Bar75] | Henk Barendregt. Open problems. In Corrado Böhm, editor, Lambda Calculus and Computer Science Theory, volume 37 of Lecture Notes in Computer Science, pages 367-370. Springer-Verlag, 1975. |
| [Bar84] | Henk Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, Amsterdam, second edition, 1984. |
| [Bar90] | Franco Barbanera. Combining term rewriting and type assignment systems. IJFCS, 1:165-184, 1990. |
| [Bar91] | Henk Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science. Oxford University Press, Oxford, 1991. To appear. |
| [Bau85] | G. Bauer. n-level rewriting systems. Theoretical Computer Science, 40:85-99, 1985. |
| [BB92] | Alessandro Berarducci and Corrado Böhm. A self-interpreter of lambda calculus having a normal form. Rapporto tecnico 16, Dip. di Matematica Pura ed Applicata, Universita di L'Aquila, October 1992. |
| [BC87] | Michel Bauderon and Bruno Courcelle. Graph expressions and graph rewritings. Mathematical Systems Theory, 20(2-3):83-127, 1987. |
| [BC92] | Alexandre Boudet and Evelyne Contejean. On n-syntactic equational theories. In H. Kirchner and G. Levi, editors, Proceedings of the Third International Conference on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 446-457, Pisa, Italy, September 1992. Springer-Verlag. |
| [BC93] | Alexandre Boudet and Hubert Comon. About the theory of tree embedding. In Gaudel and Jouannaud [GJ93]. |
| [BC94] | Alexandre Boudet and Evelyne Contejean. “Syntactic” AC-unification. In Jouannaud [Jou94], pages 136-151. [ .html ] |
| [BC97] | Alexandre Boudet and Evelyne Contejean. AC-unification of higher-order patterns. In Smolka [Smo97], pages 267-281. [ .html | .ps.gz ] |
| [BCD90] | Alexandre Boudet, Evelyne Contejean, and Hervé Devie. A new AC unification algorithm with an algorithm for solving diophantine equations. In Mitchell [Mit90], pages 289-299. |
| [BD87] | Leo Bachmair and Nachum Dershowitz. Inference rules for rewrite-based first-order theorem proving. In Second Symposium on Logic in Computer Science [87], pages 331-337. |
| [BD92] | Leo Bachmair and Nachum Dershowitz. Equational inference, canonical proofs, and proof orderings. Report DCS-R-92-1746, Department of Computer Science, University of Illinois, Urbana, IL, April 1992. |
| [BD97] | Michel Bidoit and Max Dauchet, editors. Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, Lille, France, April 1997. Springer-Verlag. |
| [Ber94] | A. Bertrand. Sur une conjecture d'Yves Métivier. Theoretical Computer Science, 123(1):21-30, 1994. |
| [BF93a] | Franco Barbanera and Maribel Fernández. Combining first and higher order rewrite systems with type assignment systems. In TLCA93 [TLC93]. |
| [BF93b] | Franco Barbanera and Maribel Fernández. Modularity of termination and confluence in combinations of rewrite systems with λω. In Lingas et al. [LKC93]. |
| [BFG94] | Franco Barbanera, Maribel Fernández, and Herman Geuvers. Modularity of strong normalization and confluence in the λ-algebraic-cube. In Abramsky [Abr94]. |
| [BGNR99] | Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, and Albert Rubio. Paramodulation with non-monotonic orderings. In Fourteenth IEEE Annual Symposium on Logic in Computer Science [99]. [ .ps.gz ] |
| [BGT91] | Horst Bunke, T. Glauser, and T.-H. Tran. An efficient implementation of graph grammars based on the RETE-matching algorithm. In H. Ehrig, H.-J. Kreowski, and G. Rozenberg, editors, Graph Grammars and Their Application to Computer Science, volume 532 of Lecture Notes in Computer Science, pages 174-189, 1991. |
| [BGW93] | Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Set constraints are the monadic class. In Vardi [Var93], pages 75-83. |
| [BGZ98] | Lubos Brim, Jozef Gruska, and Jirí Zlatuska, editors. Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, Brno, Czech Republic, August 1998. Springer-Verlag. |
| [BHW92] | Wolfgang Bibel, S. Hölldobler, and Jörg Würtz. Cycle unification. In Kapur [Kap92], pages 94-108. |
| [BJBR91] | E. Börger, G. Jäger, H. Kleine Büning, and M. M. Richter, editors. volume 626 of Lecture Notes in Computer Science, Berne, Switzerland, October 1991. Springer-Verlag. |
| [BK80] | W. Bibel and R. Kowalski, editors. 5th International Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, Les Arcs, France, 1980. Springer-Verlag. |
| [BK86a] | J. A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluency and termination. Journal of Computer and System Sciences, 32(3):323-362, 1986. |
| [BK86b] | W. Bibel and R. Kowalski, editors. 10th German Wokshop on Artificial Intelligence, Informatik Fachberichte vol. 124, Ottenstein/Niederösterreich, 1986. Springer-Verlag. |
| [BL79] | Gérard Berry and Jean-Jacques Lévy. Mimimal and optimal computations of recursive programs. J. of the Association for Computing Machinery, 26:148-175, 1979. |
| [Bla03] | Frédéric Blanqui. Definitions by rewriting in the Calculus of Constructions, 2003. To appear in Mathematical Structures in Computer Science. |
| [BO93] | R. V. Book and Friedrich Otto. String-Rewriting Systems. Springer-Verlag, 1993. |
| [Boo91] | Ronald. V. Book, editor. 4th International Conference on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, Como, Italy, April 1991. Springer-Verlag. |
| [Bou90] | Alexandre Boudet. Unification in combination of equational theories: An efficient algorithm. In Proceedings of the Tenth International Conference on Automated Deduction (Kaiserslautern, Germany), volume 449 of Lecture Notes in Computer Science. Springer-Verlag, 1990. |
| [Bou92] | Alexandre Boudet. Unification in order-sorted algebras with overloading. In Kapur [Kap92]. |
| [BPSW06] | Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors. Automata, Languages and Programming, 33rd International Colloquium, Part II, volume 4052 of Lecture Notes in Computer Science, Venice, Italy, July 2006. Springer-Verlag. |
| [BPW89] | Timothy Baird, Gerald Peterson, and Ralph Wilkerson. Complete sets of reductions modulo Associativity, Commutativity and Identity. In Dershowitz [Der89], pages 29-44. |
| [BR91] | Francois Bronsard and Uday S. Reddy. Conditional rewriting in Focus. In Okada [Oka91]. |
| [BR93] | F. Bronsard and U. S. Reddy. Reduction techniques for first-order reasoning. In Michaël Rusinowitch and Rémy [MRR93], pages 242-256. |
| [Bro95] | Francois Bronsard. Using Term Orders to Control Deductions. PhD thesis, University of Illinois, 1995. Forthcoming. |
| [BS86] | J. Richard Büchi and Steven Senger. Coding in the existential theory of concatenation. Archiv math. Logik, 26:101-106, 1986. |
| [BS92] | Franz Baader and Klaus Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Kapur [Kap92]. |
| [BS93a] | Franz Baader and Klaus Schulz. Combination techniques and decision problems for disunification. In Kirchner [Kir93], pages 301-315. |
| [BS93b] | Andrzej M. Borzyszkowski and Stefan Sokolowski, editors. Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, Gdańsk, Poland, 30 August-3 September 1993. Springer-Verlag. |
| [BS95a] | Franz Baader and Klaus Schulz. Combination of constraint solving techniques: An algebraic point of view. In Hsiang [Hsi95], pages 352-366. |
| [BS95b] | Franz Baader and Klaus Schulz. On the combination of symbolic constraints, solution domains, and constraint solvers. In Montanari and Rossi [MR95]. |
| [BS98] | Franz Baader and Klaus Schulz. Combination of constraint solvers for free and quasi-free structures. Theoretical Computer Science, 1998. To appear. |
| [BTG89] | Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic strong normalization. In 16th International Colloquium on Automata, Languages and Programming [ica89], pages 137-150. |
| [Bun94] | A. Bundy, editor. 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Computer Science, Nancy, France, 1994. Springer-Verlag. |
| [BvG+87] | Henk Barendregt, M. C. J. D. van Eekelen, J. R. W. Glauert, J. R. Kennaway, M. J. Plasmeijer, and M. R. Sleep. Term graph rewriting. In Proceedings of the European Workshop on Parallel Architectures and Languages, volume 259 of Lecture Notes in Computer Science, pages 141-158, Berlin, 1987. Springer-Verlag. |
| [BW97] | Manuel Bronstein and Volker Weispfenning, editors. Proceedings of the Conference on Symbolic Rewriting Techniques, Monte Verita, Switzerland, 1997. |
| [caa91] | Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science. Springer-Verlag, 1991. |
| [Car91] | Anne-Cécile Caron. Linear bounded automata and rewrite systems: Influence of initial configurations on decision properties. In Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 1: Colloquium on Trees in Algebra and Programming (Brighton, U.K.), volume 493 of Lecture Notes in Computer Science, pages 74-89, Berlin, April 1991. Springer-Verlag. |
| [CCD93] | Anne-Cécile Caron, Jean-Luc Coquidé, and Max Dauchet. Encompassment properties and automata with constraints. In Kirchner [Kir93], pages 328-342. |
| [CGN01] | Hubert Comon, Guillem Godoy, and Robert Nieuwenhuis. The confluence of ground term rewrite systems is decidable in polynomial time. In FOCS01 [FOC01], pages 298-307. |
| [Che81] | Paul Chew. Unique normal forms in term rewriting systems with repeated variables. In Proceedings of the Thirteenth Annual Symposium on Theory of Computing, pages 7-18. ACM, 1981. |
| [CHL92] | Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. RR 1617, Institut National de Rechereche en Informatique et en Automatique, Rocquencourt, France, February 1992. |
| [Chr] | Jim Christian. Problem corner: An experiment with Grau's ternary Boolean algebra. Submitted. |
| [Cic90] | E. A. Cichon. Bounds on derivation lengths from termination proofs. Technical Report CSD-TR-622, Department of Computer Science, University of London, Surrey, England, June 1990. |
| [CJ91] | Christian Choffrut and Matthias Jantzen, editors. Eighth Symposium on Theoretical Aspects of Computer Science, volume 480 of Lecture Notes in Computer Science, Hamburg, Germany, February 1991. Springer-Verlag. |
| [CJ97a] | Hubert Comon and Florent Jacquemard. Ground reducibility is EXPTIME-complete. In Winskel [Win97], pages 26-34. |
| [CJ97b] | Hubert Comon and Yan Jurski. Higher-order matching and tree automata. In Nielsen and Thomas [NT97], pages 157-176. |
| [CJ03] | Hubert Comon and Florent Jacquemard. Ground reducibility is EXPTIME-complete. Information and Computation, 187(1):123-153, 2003. |
| [CK84] | M. P. Chytil and V. Koubek, editors. Mathematical Foundations of Computer Science, volume 175 of Lecture Notes in Computer Science, Praha, Czechoslovakia, September 1984. Springer-Verlag. |
| [CK02] | Bruno Courcelle and Teodor Knapik. The evaluation of first-order substitution is monadic second-order compatible. Theoretical Computer Science, 281(1-2):177-206, June 2002. |
| [CL87] | Ahlem Ben Cherifa and Pierre Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137-159, October 1987. |
| [Cla96] | Edmund C. Clarke, editor. Eleventh Symposium on Logic in Computer Science, New Brunswick, NJ, July 1996. IEEE. |
| [CNNR98] | Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, and Michaël Rusinowitch. Decision problems in ordered rewriting. In Pratt [Pra98]. |
| [Com88] | Hubert Comon. Unification et Disunification: Théorie et Applications. PhD thesis, Institut National Polytechnique de Grenoble, 1988. In French. |
| [Com90] | Hubert Comon. Solving inequations in term algebras (Preliminary version). In Mitchell [Mit90], pages 62-69. |
| [Com91] | Hubert Comon. Completion of rewrite systems with membership constraints. Rapport de Recherche 699, L.R.I., Université de Paris-Sud, September 1991. |
| [Com92] | Hubert Comon. Completion of rewrite systems with membership constraints. In Kuich [Kui92], pages 392-403. |
| [Com93a] | Hubert Comon. Complete axiomatizations of some quotient term algebras. Theoretical Computer Science, 118(2), September 1993. |
| [Com93b] | Hubert Comon. Personal communication, 1993. |
| [Com97] | Hubert Comon, editor. 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, Barcelona, Spain, June 1997. Springer-Verlag. |
| [Com98a] | Hubert Comon. Completion of rewrite systems with membership constraints. Part I: Deduction rules. Journal of Symbolic Computation, 25:397-419, 1998. |
| [Com98b] | Hubert Comon. Completion of rewrite systems with membership constraints. Part II: Constraint solving. Journal of Symbolic Computation, 25:421-453, 1998. |
| [Con92] | Evelyne Contejean. Eléments pour la Décidabilité de l'Unification modulo la Distributivité. PhD thesis, Universit\'e Paris-Sud, Orsay, France, April 1992. |
| [Con93a] | Evelyne Contejean. A partial solution for D-unification based on a reduction to AC1-unification. In Proceedings of the EATCS International Conference on Automata, Languages and Programming, pages 621-632, Lund, Sweden, July 1993. Springer-Verlag. [ .html ] |
| [Con93b] | Evelyne Contejean. Solving linear Diophantine constraints incrementally. In Warren [War93], pages 532-549. [ .html ] |
| [Cou94] | Bruno Courcelle. Monadic-second order graph transductions: A survey. Theoretical Computer Science, 126:53-75, 1994. |
| [Cou97] | Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In G. Rozenberg, editor, Handbook of graph grammars and computing by graph transformations, vol. 1: Foundations, chapter 5, pages 313-400. World Scientific, New-Jersey, London, 1997. |
| [CP94a] | W. Charatonik and L. Pacholski. Negative set constraints with equality. In Abramsky [Abr94], pages 128-136. |
| [CP94b] | W. Charatonik and L. Pacholski. Set constraints with projections are in NEXPTIME. In FOCS94 [FOC94], pages 642-653. |
| [CRRT96] | C. M. Campbell, E. F. Robertson, N. Ruskuc, and M. R. Thomas. On subsemigroups and ideals in free products of semigroups. Int. J. of Algebra and Computation, 6:571-591, 1996. |
| [CSTT99] | Anne-Cécile Caron, Franck Seynhaeve, Sophie Tison, and Marc Tommasi. Deciding the satisfiability of quantifier free formulae on one-step rewriting. In Narendran and Rusinowitch [NR99], pages 103-117. |
| [CT97] | Hubert Comon and Ralf Treinen. The first-order theory of lexicographic path orderings is undecidable. Theoretical Computer Science, 176(1-2):67-87, April 1997. |
| [CW91] | D. Cohen and Phil Watson. An efficient representation of arithmetic for term rewriting. In Book [Boo91], pages 240-251. |
| [Dau89] | Max Dauchet. Simulation of Turing machines by a left-linear rewrite rule. In Dershowitz [Der89], pages 109-120. |
| [Dau92] | Max Dauchet. Simulation of Turing machines by a regular rewrite rule. Theoretical Computer Science, 103(2):409-420, 1992. |
| [de 90] | Roel C. de Vrijer. Unique normal forms for Combinatory Logic with parallel conditional, a case study in conditional rewriting. Technical report, Free University, Amsterdam, 1990. |
| [Dem80] | Piotr Dembinski, editor. Mathematical Foundations of Computer Science, Rydzyna, Poland, September 1980. |
| [Der87] | Nachum Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1&2):69-115, February/April 1987. Corrigendum: 4, 3 (December 1987), 409-410; reprinted in Rewriting Techniques and Applications, J.-P. Jouannaud, ed., pp. 69-115, Academic Press, 1987. |
| [Der89] | Nachum Dershowitz, editor. Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, Chapel Hill, NC, USA, April 1989. Springer-Verlag. |
| [Der97] | Nachum Dershowitz. Innocuous constructor-sharing combinations. In Comon [Com97], pages 202-216. |
| [Der05] | Nachum Dershowitz. Open. Closed. Open. In Giesl [Gie05]. [ .pdf ] |
| [Dev91] | Hervé Devie. Une approche algébrique de la réécriture de preuves équationnelles et son application à la dérivation de procédures de complétion. PhD thesis, Universit\'e Paris-Sud, Orsay, France, October 1991. |
| [Dev93] | Phillipe Devienne. Personal communication, 1993. |
| [dG00a] | Philippe de Groote. Linear higher-order matching is NP-complete. In Bachmair [Bac00], pages 127-140. |
| [DG00b] | Dan Dougherty and Claudio Gutiérrez. Normal forms and reduction for theories of binary relations. In Bachmair [Bac00], pages 95-109. |
| [DH95] | Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, 142:170-207, 1995. |
| [DHLT90] | Max Dauchet, Thierry Heuillard, Pierre Lescanne, and Sophie Tison. Decidability of the confluence of finite ground term rewriting systems and of other related term rewriting systems. Information and Computation, 88(2):187-201, October 1990. |
| [Die02] | Volker Diekert. Makanin's algorithm. In Lothaire [Lot02], chapter 12, pages 387-442. [ .ps ] |
| [DJ90] | Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243-320. North-Holland, Amsterdam, 1990. |
| [DJK91] | Nachum Dershowitz, Jean-Pierre Jouannaud, and Jan Willem Klop. Open problems in rewriting. In Book [Boo91], pages 445-456. |
| [DJK95] | Nachum Dershowitz, Jean-Pierre Jouannaud, and Jan Willem Klop. Problems in rewriting III. In Hsiang [Hsi95], pages 457-471. |
| [DKP91] | Nachum Dershowitz, Stéphane Kaplan, and David A. Plaisted. Rewrite, rewrite, rewrite, rewrite, rewrite,.... Theoretical Computer Science, 83(1):71-96, 1991. |
| [DKR94] | E. Domenjoud, F. Klay, and C. Ringeissen. Combination techniques for non-disjoint equational theories. In Bundy [Bun94], pages 267-281. |
| [DL94a] | Nachum Dershowitz and N. Lindenstrauss, editors. Proceedings of the Fourth International Workshop on Conditional Rewriting Systems, Jerusalem, Israel, July 1994. Springer-Verlag. |
| [DL94b] | Nachum Dershowitz and Naomi Lindenstrauss. Abstract and-parallel machines. Technical report, Department of Computer Science, Hebrew University, 1994. |
| [DMT85] | Nachum Dershowitz, Leo Marcus, and Andrzej Tarlecki. Existence, uniqueness, and construction of rewrite systems. Technical Report ATR-85(8354)-7, Computer Science Laboratory, The Aerospace Corporation, El Segundo, CA, December 1985. |
| [DO89] | J. Díaz and F. Orejas, editors. volume 1 - Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming of Lecture Notes in Computer Science, Barcelona, Spain, March 1989. Springer-Verlag. |
| [DO90] | Nachum Dershowitz and Mitsuhiro Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111-138, 1990. |
| [Dou91] | Daniel Dougherty. Adding algebraic rewriting to the untyped lambda calculus (extended abstract). In Book [Boo91], pages 37-48. |
| [Dow93] | Gilles Dowek. Third order matching is decidable. Annals of Pure and Applied Logic, 1993. |
| [DP86] | Nachum Dershowitz and David Plaisted. Equational programming. Machine Intelligence, 11:21-56, 1986. |
| [DT90] | Max Dauchet and Sophie Tison. The theory of ground rewrite systems is decidable. In Mitchell [Mit90], pages 242-248. |
| [Dur95a] | Valery G. Durnev. Undecidability of the positive for allthere exists3-theory of a free semigroup. Siberian Mathematical Journal, 36(5):917-929, September-October 1995. English translation of [Dur95b]. |
| [Dur95b] | Valery G. Durnev. Undecidability of the positive for allthere exists3-theory of a free semigroup. Sibirskiĭ Matematicheskiĭ Zhurnal, 36(5):1067-1080, September 1995. English translation as [Dur95a]. |
| [dV89] | Roel C. de Vrijer. Extending the lambda calculus with surjective pairing is conservative. In Fourth Symposium on Logic in Computer Science [89], pages 204-215. |
| [EFNT85] | Hartmut Ehrig, Christiane Floyd, Maurice Nivat, and James W. Thatcher, editors. Proceedings of the International Joint Conference on Theory and Practice of Software Development - Colloquium on Trees in Algebra and Programming, volume 185 of Lecture Notes in Computer Science. Springer-Verlag, 1985. |
| [EFW93] | Patrice Enjalbert, Alain Finkel, and Klaus W. Wagner, editors. Symposium on Theoretical Aspects of Computer Science, volume 665 of Lecture Notes in Computer Science, Würzburg, Germany, February 1993. Springer-Verlag. |
| [Eps92] | D. B. A. Epstein. Word Processing In Groups. XJones and Bartlett Publishers, 1992. |
| [EWZ08] | Joerg Endrullis, Johannes Waldmann, and Hans Zantema. Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning, 40(2-3):195-220, 2008. |
| [Fag87] | François Fages. Associative-commutative unification. Journal of Symbolic Computation, 3(3):257-275, June 1987. Previous version in the Proceedings of the Seventh International Conference on Automated Deduction, Napa, CA, pp. 194-208 [May 1984]. |
| [Fer93] | Maribel Fernández. AC-complement problems: Validity and negation elimination. In Kirchner [Kir93], pages 358-373. |
| [FOC78] | 19th Annual Symposion on Foundations of Computer Science, Ann Arbor, Michigan, October 1978. IEEE. |
| [FOC93] | Proc. 34th Symposium on Foundations of Computer Science, Palo Alto, CA, November 1993. IEEE. |
| [FOC94] | Proceedings of the 35th Symposium on Foundations of Computer Science, 1994. |
| [FOC98] | Proceedings of the 39th Symposium on Foundations of Computer Science, 1998. |
| [FOC99] | Proceedings of the 40th Symposium on Foundations of Computer Science, New York, NY, USA, October 1999. IEEE. |
| [FOC01] | Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science (FOCS), Las Vegas, Nevada, USA, 2001. |
| [Fre93] | R. Freese. personal communication, 1993. |
| [Fri85] | Laurent Fribourg. A superposition oriented theorem prover. Theoretical Computer Science, 35:161, 1985. |
| [Fri01] | Laurent Fribourg, editor. volume 2142 of Lecture Notes in Computer Science, Paris, France, September 2001. Springer-Verlag. |
| [FS90] | Peter Freyd and Andre Scedrov. Categories and Allegories, volume 39 of North Holland Mathematical Library. North-Holland, 1990. |
| [fst02] | Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Kanpur, India, December 2002. Springer-Verlag. |
| [Fur91] | Koichi Furukawa, editor. Proceedings of the 8th International Conference on Logic Programming, Paris, France, June 1991. The MIT Press. |
| [FZ93] | M. C. F. Ferreira and Hans Zantema. Total termination of term rewriting. In Kirchner [Kir93], pages 213-227. Extended version as [FZ96]. |
| [FZ96] | M. C. F. Ferreira and Hans Zantema. Total termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing, 7(2):133-162, 1996. |
| [GA01] | Jürgen Giesl and Thomas Arts. Verification of Erlang processes by dependency pairs. Applicable Algebra in Engineering, Communication and Computing, 12(1,2):39-72, 2001. |
| [Gan96] | Harald Ganzinger, editor. 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, New Brunswick, NJ, USA, July 1996. Springer-Verlag. |
| [Gan99] | Harald Ganzinger, editor. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, Trento, Italy, July 1999. Springer-Verlag. |
| [Ger92a] | S. M. Gersten. Dehn functions and l1-norms of finite presentations. In G. Baumslag and C. F. Miller III, editors, Algorithms and Classification in Combinatorial Group Theory, volume 23 of Math. Sciences Research Institute Publ., pages 195-224. Springer-Verlag, 1992. |
| [Ger92b] | S. M. Gersten. Problems on automatic groups. In G. Baumslag and C. F. Miller III, editors, Algorithms and Classification in Combinatorial Group Theory, volume 23 of Math. Sciences Research Institute Publ., pages 225-232. Springer-Verlag, 1992. |
| [Ges90] | Alfons Geser. Relative Termination. PhD thesis, qUniversität Passau, Passau, Germany, 1990. |
| [Ges03] | Alfons Geser. Termination of string rewriting rules that have one pair of overlaps. In Nieuwenhuis [Nie03], pages 410-423. |
| [GGL00] | Healfdene Goguen and Jean Goubault-Larrecq. Sequent combinators: A Hilbert system for the lambda calculus. Mathematical Structures in Computer Science, 10:1-79, 2000. [ .ps ] |
| [Gie05] | Jürgen Giesl, editor. 16th International Conference on Rewriting Techniques, volume 3467 of Lecture Notes in Computer Science, Nara, Japan, April 2005. Springer-Verlag. |
| [Gil91] | R. Gilleron. Decision problems for term rewriting systems and recognizable tree languages. In Choffrut and Jantzen [CJ91]. |
| [GJ93] | M. C. Gaudel and J.-P. Jouannaud, editors. 4th International Joint Conference on Theory and Practice of Software Development, volume 668 of Lecture Notes in Computer Science, Orsay, France, April 1993. Springer-Verlag. |
| [GL99] | Jean Goubault-Larrecq. Conjunctive types and SKInT. In Proceedings of the TYPES'98 Workshop, Lecture Notes in Computer Science. Springer-Verlag, Bad Irsee, Germany, 1999. [ .ps ] |
| [GM87] | E. Giovanetti and C. Moiso. Notes on the elimination of conditions. In Proc. CTRS '87, LNCS 308, pages 91-97, 1987. |
| [GMOZ97] | Alfons Geser, Aart Middeldorp, Enno Ohlebusch, and Hans Zantema. Relative undecidability in the termination hierarchy of single rewrite rules. In Bidoit and Dauchet [BD97], pages 237-248. |
| [Gol81] | Warren D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225-230, 1981. |
| [Gor90] | L. Gordeev. Generalizations of the Kruskal-Friedman theorems. Journal of Symbolic Logic, 55(1):157-181, 1990. |
| [GTSKF04] | Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and S. Falke. Automated termination proofs with AProVE. In van Oostrom [vO04], pages 210-220. |
| [GTSKF06] | Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. Mechanizing and improving dependency pairs. Journal of Automated Reasoning, 37(3):155-203, 2006. |
| [GTT93a] | Rémy Gilleron, Sophie Tison, and Marc Tommasi. Solving systems of set constraints using tree automata. In Enjalbert et al. [EFW93]. |
| [GTT93b] | Rémy Gilleron, Sophie Tison, and Marc Tommasi. Solving systems of set constraints with negated subset relationships. In FOCS93 [FOC93], pages 372-380. |
| [GTV04] | Guillem Godoy, Ashish Tiwari, and Rakesh Verma. Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems. Applicable Algebra in Engineering, Communication and Computing, 15(1):13-36, June 2004. [ http ] |
| [Gur88] | Yuri Gurevich, editor. Third Symposium on Logic in Computer Science, Edinburgh, Scotland, July 1988. IEEE. |
| [Gut98] | C. Gutiérrez. Satisfiability of word equations with constants is in exponential space. In FOCS98 [FOC98]. |
| [HH93] | D. Hofbauer and M. Huber. Computing linearizations using test sets. In Michaël Rusinowitch and Rémy [MRR93], pages 287-301. |
| [HJ90] | Nevin Heintze and Joxan Jaffar. A decision procedure for a class of set constraints. In Mitchell [Mit90], pages 42-51. |
| [HK92] | Ivan M. Havel and Václav Koubek, editors. Mathematical Foundations of Computer Science, volume 629 of Lecture Notes in Computer Science, Prague, Czechoslovakia, August 1992. Springer-Verlag. |
| [HK96] | Miki Hermann and P. G. Kolaitis. Unification algorithms cannot be combined in polynomial time. In McRobbie and Slaney [MS96], pages 246-260. To appear in a special issue of Information and Computation. |
| [HL78] | Gérard Huet and Dallas S. Lankford. On the uniform halting problem for term rewriting systems. Rapport laboria 283, Institut de Recherche en Informatique et en Automatique, Le Chesnay, France, March 1978. |
| [HL79] | Gérard Huet and Jean-Jacques Lévy. Call by need computations in non-ambiguous linear term rewriting systems. Rapport Laboria 359, Institut National de Recherche en Informatique et en Automatique, Le Chesnay, France, August 1979. |
| [HL91a] | Gérard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems, I and II. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 395-443. The MIT Press, Cambridge, MA, 1991. This is a revision of [HL79]. |
| [HL91b] | Gérard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems, II. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, chapter 12, pages 415-443. The MIT Press, Cambridge, MA, 1991. |
| [HMV08] | Ramesh Hariharan, Madhavan Mukund, and V Vinay, editors. volume 2 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2008. [ DOI ] |
| [Hoo96] | Charles Hoot. Termination of Non-Simple Rewrite Systems. PhD thesis, University of Illinois, 1996. |
| [HP91] | B. Hoffmann and D. Plump. Implementing term rewriting by jungle evaluation. RAIRO Theoretical Informatics and Applications, 25(5):445-472, 1991. |
| [HR86] | Jieh Hsiang and Michaël Rusinowitch. A new method for establishing refutational completeness in theorem proving. In Siekmann [Sie86], pages 141-152. |
| [HRA96] | Michael Hanus and Mario Rodríguez-Artalejo, editors. 5th International Conference on Algebraic and Logic Programming, volume 1139 of Lecture Notes in Computer Science, Aachen, Germany, September 1996. Springer-Verlag. |
| [Hsi85] | Jieh Hsiang. Refutational theorem proving using term-rewriting systems. Artificial Intelligence, 25:255-300, March 1985. |
| [Hsi95] | Jieh Hsiang, editor. 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, Kaiserslautern, Germany, April 1995. Springer-Verlag. |
| [Hue76] | Gérard Huet. Résolution d'équations dans les langages d'ordre 1,2,...,ω. Thèse d'état, Université Paris 7, Paris, France, 1976. |
| [Hue80] | Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the Association for Computing Machinery, 27(4):797-821, October 1980. |
| [Hue81] | Gérard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Computer and System Sciences, 23(1):11-21, 1981. |
| [Hue90] | Gérard Huet, editor. Logical Foundations of Functional Programming. University of Texas at Austin Year of Programming. Addison-Wesley, Reading, MA, 1990. |
| [HW93] | Philipp Hanschke and Jörg Würtz. Satisfiability of the smallest binary program. Information Processing Letters, 45(5):237-241, April 1993. |
| [HW05] | Dieter Hofbauer and Johannes Waldmann. Termination of {aa ->bc, bb ->ac, cc ->ab}. Preprint, 2005. [ .ps.gz ] |
| [ica89] | 16th International Colloquium on Automata, Languages and Programming, volume 372 of Lecture Notes in Computer Science, Stresa, Italy, July 1989. Springer-Verlag. |
| [ijc91] | International Joint Conference on Artificial Intelligence, 1991. |
| [ijc93] | 13th International Joint Conference on Artificial Intelligence, Chambéry, France, August 1993. Morgan Kaufmann. |
| [IM91] | T. Ito and A. R. Meyer, editors. Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science. Springer-Verlag, September 1991. |
| [Int97] | Benedetto Intrigila. Non-existent statman's double fixed point combinator does not exist, indeed. Information and Computation, 137(1):35-40, 1997. |
| [iwn93] | Proceedings of the international workshop on new models of software architecture, Japan, November 1993. |
| [Jac96] | Florent Jacquemard. Automates d'arbres et Réécriture de termes. PhD thesis, Université de Paris-Sud, 1996. In French. |
| [JK84] | Jean-Pierre Jouannaud and Hélène Kirchner. Construction d'un plus petit ordre de simplification. RAIRO Theoretical Informatics, 18(3):191-207, 1984. |
| [JK86] | Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15:1155-1194, November 1986. |
| [JK89] | Jean-Pierre Jouannaud and Emmanuel Kounalis. Automatic proofs by induction in equational theories without constructors. Information and Computation, 81(1):1-33, 1989. |
| [JK91a] | Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. The MIT Press, Cambridge, MA, 1991. |
| [JK91b] | Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. The MIT Press, 1991. |
| [JM90] | Jean-Pierre Jouannaud and Claude Marché. Completion modulo associativity, commutativity and identity. In Alfonso Miola, editor, Proceedings of the International Symposium on the Design and Implementation of Symbolic Computation Systems (Capri, Italy), volume 429 of Lecture Notes in Computer Science, pages 111-120, Berlin, April 1990. Springer-Verlag. |
| [JO91a] | Jean-Pierre Jouannaud and Mitsuhiro Okada. Executable higher-order algebraic specification languages. In Kahn [Kah91], pages 350-361. |
| [JO91b] | Jean-Pierre Jouannaud and Mitsuhiro Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In J. Leach Albert, B. Monien, and M. Rodríguez Artalejo, editors, Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming (Madrid, Spain), volume 510 of Lecture Notes in Computer Science, pages 455-468, Berlin, July 1991. Springer-Verlag. |
| [Jou85] | Jean-Pierre Jouannaud, editor. IFIP International Conference on Functional Programming Languages and Computer Architecture, volume 201 of Lecture Notes in Computer Science. Springer-Verlag, 1985. |
| [Jou94] | Jean-Pierre Jouannaud, editor. First International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, München, Germany, September 1994. Springer-Verlag. |
| [JS94] | Jean-Pierre Jouannaud and Walid Sadfi. Strong sequentiality of left-linear overlapping rewrite systems. In Dershowitz and Lindenstrauss [DL94a]. |
| [Kah91] | Gilles Kahn, editor. Sixth Symposium on Logic in Computer Science, Amsterdam, The Netherlands, July 1991. IEEE. |
| [Kap92] | Deepak Kapur, editor. 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Computer Science, Saratoga Springs, NY, June 1992. Springer-Verlag. |
| [Kd89] | Jan Willem Klop and Roel C. de Vrijer. Unique normal forms for lambda calculus with surjective pairing. Information and Computation, 80:97-113, 1989. |
| [Ken89] | J. R. Kennaway. Sequential evaluation strategies for parallel-or and related reduction systems. Annals of Pure and Applied Logic, 43:31-56, 1989. |
| [Kir86] | Claude Kirchner. Computing unification algorithms. In First Symposium on Logic in Computer Science [lic86], pages 206-216. |
| [Kir93] | Claude Kirchner, editor. 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, Montreal, Canada, June 1993. Springer-Verlag. |
| [KKSd90] | J. R. Kennaway, Jan Willem Klop, M. R. Sleep, and F. J. de Vries. Transfinite reductions in orthogonal term rewriting systems. Technical Report CS-R9041, CWI, Amsterdam, 1990. |
| [KKSd91] | J. R. Kennaway, Jan Willem Klop, M. R. Sleep, and F. J. de Vries. Transfinite reductions in orthogonal term rewriting systems (Extended abstract). In Book [Boo91], pages 1-12. |
| [KL92] | Hélène Kirchner and Giorgio Levi, editors. 3th International Conference on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, Volterra, Italy, September 1992. Springer-Verlag. |
| [Klo80] | Jan Willem Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980. |
| [Klo92] | Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1-117. Oxford University Press, Oxford, 1992. |
| [KM89a] | Jan Willem Klop and Aart Middeldorp. Sequentiality in orthogonal term rewriting systems. Report CS-R8932, Centre for Mathematics and Computer Science, Amsterdam, 1989. |
| [KM89b] | N. Kuhn and Klaus Madlener. A method for enumerating cosets of a group presented by a canonical system. In Proc. ISSAC'89, pages 338-350. ACM, 1989. |
| [KM91] | Jan Willem Klop and Aart Middeldorp. Sequentiality in orthogonal term rewriting systems. Journal of Symbolic Computation, 12:161-195, 1991. |
| [KMP00] | Juhani Karhumäki, Filippo Mignosi, and Wojciech Plandowski. The expressibility of languages and relations by word equations. J. of the Association for Computing Machinery, 47(5):483-505, May 2000. |
| [KN85a] | Deepak Kapur and Paliath Narendran. An equational approach to theorem proving in first-order predicate calculus. In Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pages 1146-1153, Los Angeles, CA, August 1985. |
| [KN85b] | M. S. Krishnamoorthy and P. Narendran. On recursive path ordering. Theoretical Computer Science, 40:323-328, 1985. |
| [KNZ87] | Deepak Kapur, Paliath Narendran, and Hantao Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395-415, August 1987. |
| [KO92] | M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems with shared constructors. Theoretical Computer Science, 103:273-282, 1992. |
| [Kor86] | William Kornfeld. Equality for Prolog. In D. DeGroot and G. Lindstrom, editors, Logic Programming: Functions, Relations, and Equations, pages 279-293. Prentice-Hall, Englewood Cliffs, NJ, 1986. |
| [Koz95] | Dexter Kozen, editor. Tenth Symposium on Logic in Computer Science, San Diego, CA, June 1995. IEEE. |
| [KP82] | Laurie Kirby and Jeff Paris. Accessible independence results for Peano arithmetic. Bulletin London Mathematical Society, 14:285-293, 1982. |
| [KR89] | Stéphane Kaplan and Jean-Luc Rémy. Completion algorithms for conditional rewriting systems. In H. Aït-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2: Rewriting Techniques, pages 141-170. Academic Press, Boston, 1989. |
| [KR94] | Gregory Kucherov and Michaël Rusinowitch. On the ground reducibility problem for word rewriting systems with variables. Information Processing Letters, 1994. To appear. Earlier version appeared in the Proceedings of 1994 ACM/SIGAPP Symposium on Applied Computing, Phoenix, AZ. |
| [Kru60] | Joseph B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210-225, May 1960. |
| [KT93] | Gregory Kucherov and Mohamed Tajine. Decidability of regularity and related properties of ground normal form languages. In Michaël Rusinowitch and Rémy [MRR93], pages 272-286. |
| [KT95] | Gregory Kucherov and Mohamed Tajine. Decidability of regularity and related properties of ground normal form languages. Information and Computation, 118(1):91-100, 1995. |
| [Kuc91] | G. Kucherov. On relationship between term rewriting systems and regular tree languages. In Book [Boo91]. |
| [Kui92] | Werner Kuich, editor. 19th International Colloquium on Automata, Languages and Programming, volume 623 of Lecture Notes in Computer Science, Wien, Austria, July 1992. Springer-Verlag. |
| [Kur90] | W. Kurth. Termination und Konfluenz von Semi-Thue-Systems mit nur einer Regel. PhD thesis, Technische Universitat Clausthal, Clausthal, Germany, 1990. In German. |
| [K89] | I. Kříž. Well-quasiordering finite trees with gap-condition. proof of Harvey Friedman's conjecture. Ann. of Math., 130:215-226, 1989. |
| [KV00] | Konstantin Korovin and Andrei Voronkov. A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering. In 15th Annual IEEE Symposium on Logic in Computer Science [00], pages 291-302. |
| [KV01] | Konstantin Korovin and Andrei Voronkov. Knuth-Bendix constraint solving is NP-complete. In Orejas et al. [OSvL01], pages 979-992. |
| [KV02a] | Konstantin Korovin and Andrei Voronkov. The decidability of the first-order theory of the Knuth-Bendix orders in the case of unary signatures. In Ringeissen et al. [RTTV02], pages 45-46. |
| [KV02b] | Konstantin Korovin and Andrei Voronkov. The decidability of the first-order theory of the Knuth-Bendix orders in the case of unary signatures. In Foundations of Software Technology and Theoretical Computer Science [fst02]. A preliminary report of the result appeared in [KV02a]. |
| [LA96] | Jordi Levy and Jaume Agustí. Bi-rewriting systems. Journal of Symbolic Computation, 22(3):279-314, September 1996. |
| [lac01] | Logical Aspects of Computational Linguistics, Grenoble, France, 2001. |
| [Lan79] | Dallas S. Lankford. On proving term rewriting systems are Noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech. University, Ruston, LA, May 1979. Revised October 1979. |
| [Las87] | Jean-Louis Lassez, editor. Proceedings of the Fourth International Conference on Logic Programming. The MIT Press, May 1987. |
| [Lep01] | Ingo Lepper. Simplification Orders in Term Rewriting. PhD thesis, Universität Münster, Germany, 2001. Available at http://wwwmath.uni-muenster.de/logik/publ/diss/9.html. [ .html ] |
| [Lep04] | Ingo Lepper. Simply terminating rewrite systems with long derivations. Archive for Mathematical Logic, 43(1):1-18, 2004. |
| [Les87] | Pierre Lescanne, editor. Rewriting Techniques and Applications, volume 256 of Lecture Notes in Computer Science, Bordeaux, France, May 1987. Springer-Verlag. |
| [Les90] | Pierre Lescanne. Well rewrite orderings. In Mitchell [Mit90], pages 239-256. |
| [Les92] | Pierre Lescanne. Termination of rewrite systems by elementary interpretations. In Kirchner and Levi [KL92], pages 21-36. |
| [Les94] | Pierre Lescanne. On termination of one rule rewrite systems. Theoretical Computer Science, 132(1-2):395-401, September 1994. |
| [Lev96] | Jordi Levy. Linear second-order unification. In Ganzinger [Gan96], pages 332-346. |
| [lic86] | First Symposium on Logic in Computer Science, Cambridge, MA, June 1986. IEEE. |
| [LKC93] | Andrzej Lingas, Rolf Karlsson, and Svante Carlsson, editors. 20th International Colloquium on Automata, Languages and Programming, volume 700 of Lecture Notes in Computer Science, Lund, Sweden, July 1993. Springer-Verlag. |
| [LM87] | J.-L. Lassez and K. G. Marriott. Explicit representation of terms defined by counter examples. Journal of Automated Reasoning, 3(3):1-17, September 1987. |
| [LM93] | D. Lugiez and J.-L. Moysset. Complement problems and tree automata in AC-like theories. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (Würzburg, Germany), Lecture Notes in Computer Science, Berlin, 1993. Springer-Verlag. |
| [LMSar] | Igor Litovski, Yves Métivier, and Eric Sopena. Definitions and comparisons of local computations on graphs. Mathematical Systems Theory, to appear. Available as internal report 91-43 of LaBRI, University of Bordeaux 1. |
| [LO88] | Lusk and Overbeek, editors. 9th International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, Argonne, Illinois, May 1988. Springer-Verlag. |
| [Lot02] | M. Lothaire, editor. Algebraic Combinatorics on Words. Cambridge University Press, 2002. |
| [Lov82] | D. W. Loveland, editor. 6th International Conference on Automated Deduction, volume 138 of Lecture Notes in Computer Science, New York, USA, 1982. Springer-Verlag. |
| [lpa10] | volume 6397 of ARCoSS, October 2010. To appear. |
| [LR99] | Sébastien Limet and Pierre Réty. A new result about the decidability of the existential one-step rewriting theory. In Narendran and Rusinowitch [NR99], pages 118-132. |
| [LRA94] | Giorgio Levi and Mario Rodríguez-Artalejo, editors. 4th International Conference on Algebraic and Logic Programming, volume 850 of Lecture Notes in Computer Science, Madrid, Spain, September 1994. Springer-Verlag. |
| [LRD94] | Pierre Lescanne and J. Rouyer-Degli. The calculus of explicit substitutions λυ. Technical Report RR-2222, INRIA-Lorraine, January 1994. |
| [LV00] | Jordi Levy and Mateu Villaret. Linear second-order unification and context unification with tree-regular constraints. In Bachmair [Bac00], pages 156-171. |
| [LV02] | Jordi Levy and Mateu Villaret. Currying second-order unification problems. In Tison [Tis02], pages 326-339. |
| [Lyn10] | Christopher Lynch, editor. volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), Edinburgh, UK, July 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. |
| [Mah88] | Michael J. Maher. Complete axiomatizations of the algebras of the finite, rational and infinite trees. In Gurevich [Gur88], pages 348-357. |
| [Mak77] | G. S. Makanin. The problem of solvability of equations in a free semi-group. Math. USSR Sbornik, 32(2):129-198, 1977. |
| [Man93] | Ken Mano, September 1993. Personal communication. |
| [Mar94] | M. Marchiori. Modularity of UN-> for left-linear term rewriting systems. Technical report, CWI, Amsterdam, 1994. |
| [Mar96a] | Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253-288, March 1996. [ .ps.gz ] |
| [Mar96b] | M. Marchiori. Unravelings and ultra-properties. In Proc. ALP '96, LNCS 1139, pages 107-121, 1996. |
| [Mar97] | Jerzy Marcinkowski. Undecidability of the first order theory of one-step right ground rewriting. In Comon [Com97], pages 241-253. |
| [Mar99] | Jerzy Marcinkowski. Undecidability of the there exists*for all* part of the theory of ground term algebra modulo an AC symbol. In Narendran and Rusinowitch [NR99], pages 92-102. |
| [McC97] | William McClune, editor. 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Artificial Intelligence, Townsville, Australia, July 1997. Springer-Verlag. |
| [Mel95] | Paul-André Melliès. Typed λ-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications [tlc95]. |
| [Mel96] | Paul-André Melliès. Description Abstraite des Systèmes de Réécriture. Thèse de doctorat, Université Paris VII, 20 Décembre 1996. |
| [Mét85] | Yves Métivier. Calcul de longueurs de chaînes de réécriture dans le monoïde libre. Theoretical Computer Science, 35(1):71-87, January 1985. |
| [MG95] | Aart Middeldorp and Bernhard Gramlich. Simple termination is difficult. Applicable Algebra in Engineering, Communication and Computing, 6(2):115-128, 1995. |
| [Mid89] | Aart Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Dershowitz [Der89], pages 263-277. |
| [Mid90] | Aart Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Vrije Universiteit, Amsterdam, The Netherlands, 1990. |
| [Mid93] | Aart Middeldorp. Modular properties of conditional term rewriting systems. Information and Computation, 104(1):110-158, 1993. |
| [Mid01] | Aart Middeldorp, editor. Rewriting Techniques and Applications, volume 2051 of Lecture Notes in Computer Science, Utrecht, The Netherlands, May 2001. Springer-Verlag. |
| [Mil91] | Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In P. Schroeder-Heister, editor, Extensions of Logic Programming, volume 690 of Lecture Notes in Computer Science. Springer-Verlag, 1991. |
| [Mil93] | Dale Miller, editor. Proceedings of the 1993 International Symposium on Logic Programming, Vancouver, Canada, October 1993. The MIT Press. |
| [Mit90] | John C. Mitchell, editor. Fifth Symposium on Logic in Computer Science, Philadelphia, PA, June 1990. IEEE. |
| [MO94] | K. Mano and M. Ogawa. A new proof of Chew's theorem. Technical report, IPSJ PRG94-19-7, 1994. |
| [Mos09] | Georg Moser. The Hydra battle and Cichon's principle. Applicable Algebra in Engineering, Communication and Computing, 20(2):133-158, 2009. doi:10.1007/s00200-009-0094-4. [ http ] |
| [MR84] | A. Martelli and G. Rossi. Efficient unification with infinite terms in logic programming. In International conference on fifth generation computer systems, pages 202-209, 1984. |
| [MR95] | Ugo Montanari and Francesca Rossi, editors. Principles and Practice of Constraint Programming, volume 976 of Lecture Notes in Computer Science, Cassis, France, September 1995. Springer-Verlag. |
| [MRR93] | M. Michaël Rusinowitch and J. L. Rémy, editors. Proceedings of the Third International Workshop on Conditional Rewriting Systems, volume 656 of Lecture Notes in Computer Science, Pont-à-Mousson, France, January 1993. Springer-Verlag. |
| [MS96] | M. A. McRobbie and J. K. Slaney, editors. 13th International Conference on Automated Deduction, Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996. Springer-Verlag. |
| [MSA88] | Jürgen Müller and Rolf Socher-Ambrosius. Topics in completion theorem proving. SEKI-Report SR-88-13, Fachbereich Informatik, University of Kaiserslautern, Kaiserslautern, West Germany, 1988. To appear in J. of Symbolic Computation. |
| [MSW08] | Georg Moser, Andreas Schnabl, and Johannes Waldmann. Complexity analysis of term rewriting based on matrix and context dependent interpretations. In Hariharan et al. [HMV08], pages 304-315. [ http ] |
| [MT91] | Aart Middeldorp and Yoshihito Toyama. Completeness of combinations of constructor systems. In Book [Boo91], pages 174-187. |
| [Mül92] | Fritz Müller. Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters, 41:293-299, April 1992. |
| [Muñ96] | César Muñoz. Confluence and preservation of strong normalisation in an explicit substitutions calculus (extended abstract). In Clarke [Cla96], pages 440-447. |
| [Nie93a] | Robert Nieuwenhuis. A precedence-based total AC-compatible ordering. In Kirchner [Kir93], pages 374-388. |
| [Nie93b] | Robert Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters, 47:65-69, 1993. |
| [Nie03] | Robert Nieuwenhuis, editor. 14th International Conference on Rewriting Techniques, volume 2706 of Lecture Notes in Computer Science, Valencia, Spain, June 2003. Springer-Verlag. |
| [Nie05] | Robert Nieuwenhuis, editor. 20th International Conference on Automated Deduction, volume 3632 of Lecture Notes in Computer Science, Tallinn, Estonia, July 2005. Springer-Verlag. |
| [Nip91] | Tobias Nipkow. Higher-order critical pairs. In Kahn [Kah91], pages 342-349. |
| [Nip98] | Tobias Nipkow, editor. 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, Tsukuba, Japan, April 1998. Springer-Verlag. |
| [NM90] | K. V. Nori and C. E. Veni Madhavan, editors. Foundations of Software Technology and Theoretical Computer Science, volume 472 of Lecture Notes in Computer Science, Bangalore, India, 1990. Springer-Verlag. |
| [NO90] | Robert Nieuwenhuis and Fernando Orejas. Clausal rewriting. In S. Kaplan and M. Okada, editors, Extended Abstracts of the Second International Workshop on Conditional and Typed Rewriting Systems, pages 81-88, Montreal, Canada, June 1990. Concordia University. Revised version to appear in Lecture Notes in Computer Science, Springer-Verlag, Berlin. |
| [NPR97] | Joachim Niehren, Manfred Pinkal, and Peter Ruhrberg. On equality up-to constraints over finite trees, context unification and one-step rewriting. In McClune [McC97], pages 34-48. |
| [NR99] | Paliath Narendran and Michael Rusinowitch, editors. 10th International Conference on Rewriting Techniques and Applications, volume 1631 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag. |
| [NT97] | M. Nielsen and Wolfgang Thomas, editors. volume 1414 of Lecture Notes in Computer Science, Aarhus, Denmark, August 1997. Springer-Verlag. |
| [NZM10] | Friedrich Neurauter, Harald Zankl, and Aart Middeldorp. Revisiting matrix interpretations for polynomial derivational complexity of term rewriting. In 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning [lpa10]. To appear. |
| [OCM00] | Enno Ohlebusch, Claus Claves, and Claude Marché. TALP: A tool for the termination analysis of logic programs. In Bachmair [Bac00], pages 270-273. |
| [O'D85] | Michael J. O'Donnell. Equational Logic as a Programming Language. The MIT Press, Cambridge, MA, 1985. |
| [Oga95] | M. Ogawa. Simple gap termination on term graph rewriting systems. In Theory of Rewriting Systems and Its Application, pages 99-108, 1995. Research report 918, RIMS, Kyoto Univ, Kyoto., also available at http://www.brl.ntt.co.jp/people/mizuhito. |
| [Ohl94a] | Enno Ohlebusch. On the modularity of confluence of constructor-sharing term rewriting systems. In 19th Colloquium on Trees in Algebra and Programming, volume 787 of LNCS, pages 261-275. Springer-Verlag, 1994. |
| [Ohl94b] | Enno Ohlebusch. On the modularity of confluence of constructor-sharing term rewriting systems. In Tison [Tis94]. |
| [Ohl97] | Enno Ohlebusch. Conditional term graph rewriting. In 6th International Conference on Algebraic and Logic Programming [alp97], pages 144-158. [ http ] |
| [Ohl01] | Enno Ohlebusch. Termination of logic programs: Transformational methods revisited. Applicable Algebra in Engineering, Communication and Computing, 12(1,2):73-116, 2001. |
| [Ohs01] | Hitoshi Ohsaki. Beyond regularity: Equational tree automata for associative and commutative theories. In Fribourg [Fri01], pages 539-553. |
| [Oka91] | M. Okada, editor. Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, volume 516 of Lecture Notes in Computer Science, Montreal, Canada, 1991. Springer-Verlag. |
| [Oku98] | Satoshi Okui. Simultaneous critical pairs and Church-Rosser property. In Nipkow [Nip98], pages 2-16. |
| [OO89] | M. Ogawa and S. Ono. On the uniquely converging property of nonlinear term rewriting systems. Technical report, IEICE COMP89-7, 1989. |
| [OO93] | Michio Oyamaguchi and Yoshikatsu Ohta. On the confluent property of right-ground term rewriting systems. Trans. IEICE, J76-D-I:39-45, 1993. |
| [OO97] | Michio Oyamaguchi and Yoshikatsu Ohta. A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In Comon [Com97], pages 187-201. |
| [Oos92] | V. van Oostrom. Confluence by decreasing diagrams. IR 298, Vrije Universiteit, Amsterdam, The Netherlands, August 1992. To appear in Theoretical Computer Science. |
| [Oos94] | Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994. |
| [Oos97a] | Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175:159-181, 1997. |
| [Oos97b] | Vincent van Oostrom. Finite family developments. In Comon [Com97], pages 308-322. |
| [OOTar] | Yoshikatsu Ohta, Michio Oyamaguchi, and Yoshihito Toyama. On the Church-Rosser property of simple-right-linear term rewriting systems. Trans. IEICE, to appear. |
| [OSKM98] | Friedrich Otto, Andrea Sattler-Klein, and Klaus Madlener. Automatic monoids versus monoids with finite convergent presentations. In Nipkow [Nip98], pages 32-46. |
| [OSvL01] | Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors. 28th International Colloquium on Automata, Languages and Programming, volume 2076 of Lecture Notes in Computer Science, Crete, Greece, July 2001. Springer-Verlag. |
| [OT02] | Hitoshi Ohsaki and Toshinori Takai. Decidability and closure properties of equational tree languages. In Tison [Tis02], pages 114-128. |
| [Oto12] | Jan Otop. E-unification with constants vs. general E-unification. Journal of Automated Reasoning, 48(3):363-390, March 2012. [ .pdf ] |
| [Ott87] | Thomas Ottmann, editor. 14th International Colloquium on Automata, Languages and Programming, volume 267 of Lecture Notes in Computer Science, Karlsruhe, Germany, July 1987. Springer-Verlag. |
| [OTTR05] | Hitoshi Ohsaki, Jean-Marc Talbot, Sophie Tison, and Yves Roos. Monotone AC-tree automata. In Sutcliffe and Voronkov [SV05], pages 337-351. |
| [Oya87] | Michio Oyamaguchi. The Church-Rosser property for ground term rewriting systems is decidable. Theoretical Computer Science, 49(1):43-79, 1987. |
| [Oya90] | Michio Oyamaguchi. On the word problem for right-ground term-rewriting systems. In Trans. IEICE, volume E73-5, pages 718-723, 1990. |
| [Pad96] | Vincent Padovani. Filtrage d'ordre supérieure. Phd thesis, Université de Paris 7, Paris, France, 1996. |
| [Pat90] | M. S. Paterson, editor. 17th International Colloquium on Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, Warwick, England, 1990. Springer-Verlag. |
| [Pla85] | David A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65(2/3):182-215, May/June 1985. |
| [Pla99] | Wojciech Plandowski. Satisfiability of word equations with constants is in PSPACE. In FOCS99 [FOC99], pages 495-500. |
| [Plo02] | Gordon Plotkin, editor. {{IEEE} Symposium on Logic in Computer Science, LICS 2002}, Copenhagen, Denmark, July 2002. IEEE. |
| [Plu91] | D. Plump. Implementing term rewriting by graph reduction: Termination of combined systems. In S. Kaplan and M. Okada, editors, Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems (Montreal, Canada, June 1990), volume 516 of Lecture Notes in Computer Science, pages 307-317, Berlin, 1991. Springer-Verlag. |
| [Plu93] | D. Plump. Hypergraph rewriting: Critical pairs and undecidability of confluence. In M. R. Sleep, M. J. Plasmeijer, and M. C. van Eekelen, editors, Term Graph Rewriting: Theory and Practice, chapter 15. Wiley, 1993. To appear. |
| [POD91] | Tenth ACM Symposium on the Principles of Database Systems, Denver, CO, May 1991. ACM. |
| [POP75] | Proceedings of 2nd ACM Conference on Principles of Programming Languages, Palo Alto, CA, 1975. ACM. |
| [POP80] | Proccedings of the Seventh Annual ACM Symposion on Principles of Programming Languages, Las Vegas, Nevada, January 1980. ACM. |
| [POP87] | Proceedings of the 14th ACM Conference on Principles of Programming Languages, Munich, Germany, January 1987. ACM. |
| [POP90] | Proceedings of the 17th ACM Conference on Principles of Programming Languages, San Francisco, CA, January 1990. ACM. |
| [POP91] | Proceedings of the 18th Symposium on Principles of Programming Languages, Orlando, FL, January 1991. ACM. |
| [POP92] | Conference Record of the 19th Symposium on Principles of Programming Languages, Albuquerque, NM, 1992. ACM. |
| [POP94] | Conference Record of the 21st Symposium on Principles of Programming Languages, Portland, Oregon, 1994. ACM. |
| [POP97] | Conference Record of the 21st Symposium on Principles of Programming Languages, Paris, France, January 1997. ACM. |
| [PPC94] | Principles and Practice of Constraint Programming, Orcas Island, Washington, USA, 1994. |
| [Pra98] | Vaughan Pratt, editor. Thirteenth IEEE Annual Symposium on Logic in Computer Science, Indianapolis, IN, June 1998. IEEE. |
| [PS81] | Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. J. of the Association for Computing Machinery, 28(2):233-264, April 1981. |
| [PT94] | Leszek Pacholski and Jerzy Tiuryn, editors. volume 933 of Lecture Notes in Computer Science, Kazimierz, Poland, September 1994. Springer-Verlag. |
| [QW94] | Zheniu Qian and Kang Wang. Modular AC-unification of higher-order patterns. In Jouannaud [Jou94], pages 105-120. |
| [Raa96] | Femke van Raamsdonk. Confluence and Normalization for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1996. |
| [Rao95] | M.R.K. Krishna Rao. Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems. In Theory and practice of Software Development, TAPSOFT'95, volume 915 of Lecture Notes in Computer Science, pages 379-393. Springer-Verlag, 1995. |
| [Rao98] | M.R.K. Krishna Rao. Modular aspects of term graph rewriting. Theoretical Computer Science, 208(1-2):59-86, 1998. Special issue on Rewriting Techniques and Applications conference RTA'96. |
| [Rei85] | B. Reid, editor. Proceedings of 12th ACM Conference on Principles of Programming Languages. ACM, 1985. |
| [Rin92] | Christophe Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In Voronkov [Vor92]. |
| [RS] | Neil Robertson and P. D. Seymour. Graph minors IV. Tree-width and well-quasi-ordering. Submitted 1982; revised January 1986. |
| [RS96] | Neil Robertson and P. Seymour. Graph minors 23: Nash-williams' immersion conjecture. Preprint, March 1996. |
| [RTTV02] | Christophe Ringeissen, Cesare Tinelli, Ralf Treinen, and Rakesh M. Verma, editors. Proceedings of the 16th International Workshop on Unification ({UNIF} 2002), Technical Report 02-05, Department of Computer Science, University of Iowa, Copenhagen, Denmark, July 2002. |
| [Rub94] | Albert Rubio. Automated deduction with constrained clauses. PhD thesis, Univ. de Catalunya, 1994. |
| [RV80] | Jean-Claude Raoult and Jean Vuillemin. Operational and semantic equivalence between recursive programs. J. of the Association for Computing Machinery, 27(4):772-796, October 1980. |
| [Sce92] | Andre Scedrov, editor. Seventh Symposium on Logic in Computer Science, Santa Cruz, CA, June 1992. IEEE. |
| [Sch97] | Aleksy Schubert. Linear interpolation for the higher-order matching problem. In Bidoit and Dauchet [BD97], pages 441-452. |
| [Sch02] | Kai Scheffermann. A countererexample to the modularity of unicity of normal forms for join conditional term rewriting systems. Preprint pr309, Universität Hannover, Institut für Mathematik, April 2002. [ .dvi | .ps | .pdf ] |
| [SH95] | S. Doaitse Swierstra and M. Hermenegildo, editors. 7th International Symposium on Programming Languages: Implementations, Logics and Programs, volume 982 of Lecture Notes in Computer Science, Utrecht, The Netherlands, September 1995. Springer-Verlag. |
| [Sho84] | R. E. Shostak, editor. 7th International Conference on Automated Deduction, volume 170 of Lecture Notes in Computer Science, Napa, California, USA, 1984. Springer-Verlag. |
| [Shy92] | R. Shyamasundar, editor. volume 652 of Lecture Notes in Computer Science, New Delhi, India, December 1992. Springer-Verlag. |
| [Sie86] | Jrg Siekmann, editor. 8th International Conference on Automated Deduction, volume 230 of Lecture Notes in Computer Science, Oxford, England, 1986. Springer-Verlag. |
| [Sim85] | S.G. Simpson. Nonprovability of certain combinatorial properties of finite trees. In L. A. Harrington, editor, Harvey Friedman's research on the Foundation of Mathematics, pages 87-117. Elsevier Science, 1985. |
| [Sim04] | Jakob Grue Simonsen. On confluence and residuals in Cauchy convergent transfinite rewriting. Information Processing Letters, 91(3):141-146, August 2004. [ http ] |
| [Siv89] | G. Sivakumar. Proofs and Computations in Conditional Equational Theories. PhD thesis, Department of Computer Science, University of Illinois, Urbana, IL, May 1989. Report R-89-1642. |
| [SK94] | Andrea Sattler-Klein. About changing the ordering during Knuth-Bendix completion. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 175-186, 1994. |
| [Smo97] | Gert Smolka, editor. Principles and Practice of Constraint Programming, volume 1330 of Lecture Notes in Computer Science, Linz, Austria, October 1997. Springer-Verlag. |
| [Sny91] | Wayne Snyder. A note on the complexity of simplification orderings. Technical Report TR 90-009, Boston University, Boston, MA, 1991. |
| [Squ87] | Craig Squier. Word problems and a homological finiteness condition for monoids. J. of Pure and Applied Algebra, 49:201-217, 1987. |
| [Squ91] | C. Squier. Word problems and a homological finiteness condition for monoids. Journal of Pure and Applied Algebra, 1991. |
| [SS89] | Manfred Schmidt-Schauß. Combination of unification algorithms. Journal of Symbolic Computation, 8, 1989. |
| [SS94a] | Manfred Schmidt-Schauß. Unification of stratified second-order terms. Research Report 12/94, Fachbereich Informatik, Universität Frankfurt, Germany, December 1994. |
| [SS94b] | Manfred Schmidt-Schauß. Unification of stratified second-order terms. Internal Report 12/94, Johann-Wolfgang-Goethe-Universität, Frankfurt, Germany, 1994. [ .ps.gz ] |
| [SS97] | Manfred Schmidt-Schauß. A unification algorithm for distributivity and a multiplicative unit. Journal of Symbolic Computation, 22(3):315-344, 1997. |
| [SSS98] | Manfred Schmidt-Schauß and Klaus Schulz. On the exponent of peridicity of minimal solutions of context equations. In Nipkow [Nip98], pages 61-75. |
| [SSS99a] | Manfred Schmidt-Schauß and Klaus Schulz. Solvability of context unification with two context variables is decidable. In Ganzinger [Gan99], pages 67-81. Complete version as [SSS99b]. |
| [SSS99b] | Manfred Schmidt-Schauß and Klaus Schulz. Solvability of context unification with two context variables is decidable. CIS-Report 98-114, CIS, Universität München, München, Germany, 1999. [ .ps ] |
| [Sta91] | Richard Statman. There is no hyperrecurrent S,K combinator. Research Report 91-133, Department of Mathematics, Carnegie Mellon University, Pittsburgh, PA, 1991. |
| [Sta92] | Richard Statman. A short note on a problem of Ray Smullyan. Technical report, INRIA-Rocquencourt, 1992. |
| [Sta00] | Rick Statman. On the word problem for combinators. In Bachmair [Bac00], pages 203-213. |
| [Sti90] | M. E. Stickel, editor. 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence, Kaiserslautern, Germany, July 1990. Springer-Verlag. |
| [Sti06] | Colin Stirling. A game-theoretic approach to deciding higher-order matching. In Bugliesi et al. [BPSW06], pages 348-359. |
| [Sto85] | Herbert Stoyan, editor. 9th German Wokshop on Artificial Intelligence, Informatik Fachberichte vol. 118, Dassel/Solling, 1985. Springer-Verlag. |
| [Stø05] | Kristian Støvring. Extending the extensional lambda calculus with surjective pairing is conservative. Research Report BRICS RS-05-35, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, November 2005. [ http ] |
| [Stø06] | Kristian Støvring. Extending the extensional lambda calculus with surjective pairing is conservative. Logical Methods in Computer Science, 2(2:1):1-14, 2006. [ http ] |
| [STT97] | Franck Seynhaeve, Marc Tommasi, and Ralf Treinen. Grid structures and undecidable constraint theories. In Bidoit and Dauchet [BD97], pages 357-368. |
| [STTT01] | Franck Seynhaeve, Sophie Tison, Marc Tommasi, and Ralf Treinen. Grid structures and undecidable constraint theories. Theoretical Computer Science, 258(1-2):453-490, May 2001. [ .ps.gz ] |
| [SU91] | Vijay Saraswat and Kazunori Ueda, editors. Proceedings of the 1991 International Symposium on Logic Programming, San Diego, USA, 1991. The MIT Press. |
| [SV05] | Geoff Sutcliffe and Andrei Voronkov, editors. volume 3835 of Lecture Notes in Artificial Intelligence, Montego Bay, Jamaica, December 2005. Springer-Verlag. |
| [TA87] | Erik Tiden and Stefan Arnborg. Unification problems with one-sided distributivity. Journal of Symbolic Computation, 3:183-202, 1987. |
| [Taj93] | Mohamed Tajine. Negation elimination for syntactic equational formula. In Kirchner [Kir93], pages 316-327. |
| [Tak93] | Masako Takahashi. λ-calculi with conditional rules. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications (Utrecht, The Netherlands), volume 664 of Lecture Notes in Computer Science, pages 406-417, Berlin, 1993. Springer-Verlag. |
| [tap87] | Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 2 of Lecture Notes in Computer Science, Pisa, Italy, 1987. Springer-Verlag. |
| [Tar91] | Andrzej Tarlecki, editor. Mathematical Foundations of Computer Science, volume 520 of Lecture Notes in Artificial Intelligence, Kazimierz Dolny, Poland, September 1991. Springer-Verlag. |
| [Tha87] | S. Thatte. A refinement of strong sequentiality for term rewriting with constructors. Information and Computation, 72:46-65, 1987. |
| [Tho97] | Wolfgang Thomas. Automata theory on trres and partial orders. In Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 20-38, 1997. |
| [Tis90] | Sophie Tison. Automates comme outil de décision dans les arbres. Dossier d'habilitation à diriger des recherches, December 1990. In French. |
| [Tis94] | Sophie Tison, editor. Colloquium on Trees in Algebra and Programming, volume 787 of Lecture Notes in Computer Science, Edinburgh, Scotland, 1994. Springer-Verlag. |
| [Tis02] | Sophie Tison, editor. Rewriting Techniques and Applications, volume 2378 of Lecture Notes in Computer Science, Copenhagen, Denmark, July 2002. Springer-Verlag. |
| [Tiw02] | Ashish Tiwari. Deciding confluence of certain term rewriting systems in polynomial time. In Plotkin [Plo02], pages 447-456. |
| [TLC93] | International Conference of Typed Lambda Calculi and Applications, 1993. |
| [tlc95] | Typed Lambda Calculi and Applications, 1995. |
| [TO94] | Yoshihito Toyama and Michio Oyamaguchi. Church-Rosser property and unique normal form property of non-duplicating term rewriting systems. In Dershowitz and Lindenstrauss [DL94a]. |
| [Tou97] | Hélène Touzet. Propriétés combinatoires pour la terminaison de systèmes de réécriture. PhD thesis, Université Henri Poincaré - Nancy 1, Nancy, France, September 1997. In French. [ .ps.gz ] |
| [Tou98] | Hélène Touzet. Encoding the Hydra battle as a rewrite system. In Brim et al. [BGZ98], pages 267-276. |
| [Tou99] | Hélène Touzet. A characterization of multiply recursive functions with Higman's lemma. In Narendran and Rusinowitch [NR99], pages 163-174. |
| [Toy87] | Yoshihito Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. J. of the Association for Computing Machinery, 34(1):128-143, January 1987. |
| [Toy88] | Yoshihito Toyama. Commutativity of term rewriting systems. In K. Fuchi and L. Kott, editors, Programming of Future Generation Computers II, pages 393-407. North-Holland, 1988. |
| [Toy92] | Yoshihito Toyama. Strong sequentiality of left linear overlapping term rewriting systems. In Scedrov [Sce92]. |
| [Tre90] | Ralf Treinen. A new method for undecidability proofs of first order theories. In K. V. Nori and C. E. Veni Madhavan, editors, Proceedings of the Tenth Conference on Foundations of Software Technology and Theoretical Computer Science, volume 472 of Lecture Notes in Computer Science, pages 48-62. Springer-Verlag, 1990. |
| [Tre92] | Ralf Treinen. A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14(5):437-458, November 1992. |
| [Tre96] | Ralf Treinen. The first-order theory of one-step rewriting is undecidable. In Ganzinger [Gan96], pages 276-286. [ .ps.gz ] |
| [Tre98] | Ralf Treinen. The first-order theory of linear one-step rewriting is undecidable. Theoretical Computer Science, 208(1-2):179-190, November 1998. |
| [87] | IEEE. Second Symposium on Logic in Computer Science, 1987. |
| [89] | IEEE. Fourth Symposium on Logic in Computer Science, 1989. |
| [99] | IEEE. Fourteenth IEEE Annual Symposium on Logic in Computer Science, Trento, Italy, July 1999. |
| [00] | IEEE. 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, CA, USA, June 2000. |
| [Var93] | Moshe Y. Vardi, editor. Eigth Symposium on Logic in Computer Science, Montreal, Canada, June 1993. IEEE. |
| [Ven87] | K. N. Venkataraman. Decidability of the purely existential fragment of the theory of term algebras. J. of the Association for Computing Machinery, 34(2):492-510, 1987. |
| [Ver95] | Rakesh M. Verma. Unique normal forms and confluence for rewrite systems. In Int'l Joint Conf. on Artificial Intelligence, pages 362-368, 1995. |
| [Ver96a] | Rakesh M. Verma. Unicity and modularity of confluence for term rewriting systems. Technical report, University of Houston, 1996. |
| [Ver96b] | Rakesh M. Verma. Unicity and modularity of confluence for term rewriting systems. Technical report, University of Houston, 1996. |
| [Ver97] | Rakesh M. Verma. Unique normal forms for nonlinear term rewriting systems: Root overlaps. In Symp. on Fundamentals of Computation Theory, volume 1279 of Lecture Notes in Computer Science, pages 452-462. Springer-Verlag, September 1997. |
| [VG92] | S. Vágvölgyi and R. Gilleron. For a rewrite system it is decidable whether the set of irreducible, ground terms is decidable. Bulletin of the European Association for Theoretical Computer Science, 48:197-209, October 1992. |
| [vH94] | Pascal van Hentenryck, editor. Proceedings of the Eleventh International Conference on Logic Programming, Santa Margherita Ligure, Italy, 1994. The MIT Press. |
| [Vis80] | A. Visser. Numerations, lambda calculus, and arithmetic. In Hindley and Seldin, editors, Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pages 259-284. Academic Press, 1980. |
| [vO94] | Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, March 1994. |
| [vO04] | Vincent van Oostrom, editor. 15th International Conference on Rewriting Techniques, volume 3091 of Lecture Notes in Computer Science, Aachen, Germany, June 2004. Springer-Verlag. |
| [Vor92] | A. Voronkov, editor. volume 624 of Lecture Notes in Artificial Intelligence, St. Petersburg, Russia, July 1992. Springer-Verlag. |
| [Vor93] | Andrei Voronkov, editor. volume 698 of Lecture Notes in Artificial Intelligence, St. Petersburg, Russia, July 1993. Springer-Verlag. |
| [Vor96] | Sergei Vorobyov. An improved lower bound for the elementary theories of trees. In McRobbie and Slaney [MS96], pages 275-287. |
| [Vor97a] | Sergei Vorobyov. The first-order theory of one step rewriting in linear noetheran systems is undecidable. In Comon [Com97], pages 254-268. |
| [Vor97b] | Sergei Vorobyov. The "hardest" natural decidable theory. In Winskel [Win97], pages 294-305. |
| [vOvR94] | Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In A. Nerode and Y. V. Matiyasevich, editors, Third International Symposium on the Logical Foundations of Computer Science, volume 813 of Lecture Notes in Computer Science, pages 379-392, St. Petersburg, Russia, July 1994. Springer-Verlag. |
| [VZ84] | M. Venturini-Zilli. Reduction graphs in the Lambda Calculus. Theoretical Computer Science, 29:251-275, 1984. |
| [wad94] | Proceedings 10th workshop on abstract data types (1992)., Caldes de Malevella, Spain, October 1994. Springer-Verlag. |
| [Wal97] | Johannes Waldmann. How to decide S. Forschungsergebnisse 97/03, Friedrich-Schiller-Universität Jena, Fakultät Mathematik, Jena, Germany, 1997. |
| [Wal98a] | Johannes Waldmann. The Combinator S. PhD thesis, Fakultät für Mathematik und Informatik of the Friedrich-Schiller-Universität Jena, Jena, Germany, 1998. [ http ] |
| [Wal98b] | Johannes Waldmann. Normalisation of s-terms is decidable. In Nipkow [Nip98], pages 138-150. |
| [Wal10] | Johannes Waldmann. Polynomially bounded matrix interpretations. In Lynch [Lyn10], pages 357-372. [ http ] |
| [War93] | David S. Warren, editor. Proceedings of the Tenth International Conference on Logic Programming, Logic Programming, Budapest, Hungary, June 1993. The MIT Press. |
| [WC03] | Daria Walukiewicz-Chrzaszcz. Termination of rewriting in the Calculus of Constructions. Journal of Functional Programming, 13(2):339-414, 2003. |
| [Wei92] | Andreas Weiermann. Well-rewrite orderings and the induced recursive path orderings. Unpublished note, Institut für Mathematische Logik und Grundlagenforschung, 1992. |
| [Wei93] | Andreas Weiermann. Bounding derivation lengths with functions from the slow growing hierarchy. Preprint Münster, 1993. |
| [Wel94] | Joe B. Wells. Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In Abramsky [Abr94]. |
| [Wer94] | Benjamin Werner. Méta-théorie du Calcul des Constructions Inductives. Thèse Univ. Paris VII, France, 1994. |
| [Wie99] | Tomasz Wierzbicki. Complexity of the higher-order matching. In Ganzinger [Gan99], pages 82-96. |
| [Win97] | Glynn Winskel, editor. Twelfth Symposium on Logic in Computer Science, Warsaw, Poland, June 1997. IEEE. |
| [Wos] | Larry Wos. Automated reasoning: 33 basic research problems. |
| [Wra90] | C. Wrathall. Confluence of one-rule Thue systems. In Proceedings of the First International Workshop on Word Equations and Related Topics (Tubingen), volume 572 of Lecture Notes in Computer Science, pages 237-246, Berlin, 1990. Springer-Verlag. |
| [WS90] | D.H.D. Warren and P. Szeredi, editors. Proceedings of the 7th International Conference on Logic Programming. The MIT Press, June 1990. |
| [WZ95] | H. R. Walters and Hans Zantema. Rewrite systems for integer arithmetic. In Hsiang [Hsi95], pages 324-338. |
| [YASM00] | Toshiyuki Yamada, Jürgen Avenhaus, Carlos Loría Sáenz, and Aart Middeldorp. Logicality of conditional rewrite systems. Theoretical Computer Science, 236(1-2):209-232, April 2000. [ .html ] |
| [Zan93] | Hans Zantema. Type removal in term rewriting. In Michaël Rusinowitch and Rémy [MRR93], pages 148-154. |
| [Zan94a] | Hans Zantema. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation, 17:23-50, 1994. |
| [Zan94b] | Hans Zantema. Total termination of term rewriting is undecidable. Technical Report UU-CS-1994-55, Utrecht University, December 1994. |
| [ZG96] | Hans Zantema and Alfons Geser. Non-looping rewriting. Technical Report UU-CS-96-03, Utrecht University, Department of Computer Science, January 1996. Extended version to appear in RAIRO Théor. Inf as "Non-looping string rewriting". |
| [Zha91] | Hantao Zhang. A new strategy for the Boolean ring based approach to first order theorem proving. Technical report, Department of Computer Science, University of Iowa, 1991. |
| [Zhaar] | J. Zhang. A 3-place commutative operator from TBA. AAR Newsletters, to appear. |
| [ZL03] | Silvano Dal Zilio and Denis Lugiez. XML schema, tree logic and sheaves automata. In Nieuwenhuis [Nie03], pages 246-263. |
| [ZSM05] | Ting Zhang, Henny Sipma, and Zohar Manna. The decidability of the first-order theory of Knuth-Bendix order. In Nieuwenhuis [Nie05], pages 131-148. [ .html ] |
This file was generated by bibtex2html 1.96.