Rewriting techniques and applications. 3rd international conference, RTA- 89, Chapel Hill, NC, USA, April 3-5, 1989. Proceedings. (English) Zbl 0741.68008

Lecture Notes in Computer Science. 355. Berlin etc.: Springer-Verlag (ISBN 3-540-51081-8). VII, 577 p. (1989).
[The articles of this volume will not be indexed individually.]
Term rewriting systems have intensively been studied since 1970 when Knuth and Bendix published the well-known completion procedure. Since then a great effort was made to improve the Knuth-Bendix algorithm and to apply it in different areas.
The volume contains the proceedings of the Third International Conference on Rewriting Techniques and Applications (RTA-81), which was held April 3-5, 1989, in Chapel Hill, North Carolina, USA.
The papers presented belong to the following areas: term rewriting systems, conditional rewriting, graph rewriting and grammars, algebraic semantics, equational reasoning, lambda and combinatory calculi, symbolic and algebraic computation, equational programming languages, completion procedures, rewrite-based theorem proving, unification and matching algorithms and term-based architectures.
The volume contains a lecture on “Rewriting ideas from universal algebra” by Garret Birkhoff, 34 regular papers and 12 systems descriptions. The conference includes a section devoted to term-based architectures.
Contents: Garrett Birkhoff, Rewriting ideas from universal algebra (abstract) (p. 1); Franz Baader, Characterizations of unification type zero (pp. 2-14); Leo Bachmair, Proof normalization for resolution and paramodulation (pp. 15-28); Timothy B. Baird, Gerald E. Peterson and Ralph W. Wilkerson, Complete sets of reductions modulo associativity, commutativity and identity (pp. 29-44); Hubert Bertling and Harald Ganzinger, Completion time optimization of rewrite-time goal solving (pp. 45-58); Reinhard Bündgen and Wolfgang Küchlin, Computing ground reducibility and inductively complete positions (pp. 59-75); Hubert Comon, Inductive proofs by specification transformations (pp. 76-91); John Darlington and Yi-ke Guo, Narrowing and unification in functional programming – an evaluation mechanism for absolute set abstraction (pp. 92-108); Max Dauchet, Simulation of turing machines by a left- linear rewrite rule (pp. 109-120); Conal M. Elliott, Higher-order unification with dependent function types (pp. 121-136); Stephen J. Garland and John V. Guttag, An overview of LP, the Larch prover (pp. 137-151); Herbert Göttler, Graph grammars, a new paradigm for implementing visual languages (pp. 152-166); Dieter Hofbauer and Clemens Lautemann, Termination proofs and the length of derivations (preliminary version) (pp. 167-177); Stephane Kaplan and Christine Choppy, Abstract rewriting with concrete operators (pp. 178-186); Mike Lai, On how to move mountains ‘associatively and commutatively’ (pp. 187-202); Dallas Lankford, Generalized Gröbner bases: Theory and applications. A condensation (pp. 203-221); Dana May Latch and Ron Sigal, A local termination property for term rewriting systems (pp. 222-233); George F. McNulty, An equational logic sampler (pp. 234-262); Aart Middeldorp, Modular aspects of properties of term rewriting systems related to normal forms (pp. 263-277); Chilukuri K. Mohan, Priority rewriting: Semantics, confluence, and conditionals (pp. 278-291); Chilukuri K. Mohan and Mandazam K. Srivas, Negation with logical variables in conditional rewriting (pp. 292-310); Tohru Naoi and Yasuyoshi Inagaki, Algebraic semantics and complexity of term rewriting systems (pp. 311-325); Sanjai Narain, Optimization by non-deterministic, lazy rewriting (pp. 326-342); Tobias Nipkow, Combining matching algorithms: The regular case (pp. 343-358); Friedrich Otto, Restrictions of congruences generated by finite canonical string- rewriting systems (pp. 359-370); Laurence Puel, Embedding with patterns and associated recursive path ordering (pp. 371-387); Uday S. Reddy, Rewriting techniques for program synthesis (pp. 388-403); R. C. Sekar, Shaunak Pawagi and I. V. Ramakrishnan, Transforming strongly sequential rewrite systems with constructors for efficient parallel execution (pp. 404-418); Wayne Snyder, Efficient ground comletion: An \(O(n \log n)\) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations \(E\) (pp. 419-433); Joachim Steinbach, Extensions and comparison of simplification orderings (pp. 434-448); Robert I. Strandh, Classes of equational programs that compile into efficient machine code (pp. 449- 461); Sophie Tison, Fair termination is decidable for ground systems (pp. 462-476 ); Yoshihito Toyama, Jan Willem Klop and Hendrik Pieter Barendregt, Termination for the direct sum of left- linear term rewriting systems (preliminary draft) (pp. 477-491); Sergey G. Vorobyov, Conditional rewrite rule systems with built-in arithmetic and induction (pp. 492-512); Hantao Zhang and Deepak Kapur, Consider only general superpositions in completion procedures (pp. 513-529); Habib Abdulrab and Jean-Pierre Pécuchet, Solving systems of linear diophantine equations and word equations (pp. 530-532); Siva Anantharaman, Jieh Hsiang and Jalel Mzali, SbReve2: A term rewriting laboratory with (AC- )unfailing completion (pp. 533-537); J. Avenhaus, J. Denzinger and J. Müller, THEOPOGLES – an efficient theorem prover based on rewrite-techniques (pp. 538-541); Jürgen Avenhaus, Klaus Madlener and Joachim Steinbach, COMTES – an experimental environment for the completion of term rewriting systems (pp. 542-546); Michel Bidoit, Francis Capy, Christine Choppy, Stephane Kaplan, Francoise Schlienger and Frederic Voisin, ASSPEGIQUE: An integrated specification environment (p. 547); Maria Paola Bonacina and Giancarlo Sanna, KBlab: An equational theorem prover for the Macintosh (pp. 548-550); Jim Christian, Fast Knuth-Bendix completion: Summary (pp. 551-555); M. Dauchet and A. Deruyver, Compilation of ground term rewriting systems and applications (pp. 556-558); Deepak Kapur and Hantao Zhang, An overview of rewrite rule laboratory (RRL) (pp. 559- 563); H. Khoshnevisan and K. M. Sephton, InvX: An automatic function inverter (pp. 564-568); Naomi Lindenstrauss, A parallel implementation of rewriting and narrowing (pp. 569-573); John Pedersen, Morphocompletion for one-relation monoids (pp. 574-578).


68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68Q42 Grammars and rewriting systems
00B25 Proceedings of conferences of miscellaneous specific interest