Rewriting Techniques and Applications: 3rd International Conference, RTA-89 Chapel Hill, North Carolina, USA April 3–5, 1989 Proceedings

Garrett Birkhoff (auth.), Nachum Dershowitz (eds.)3540510818, 9783540510819

Rewriting has always played an important role in symbolic manipulation and automated deduction systems. The theory of rewriting is an outgrowth of Combinatory Logic and the Lambda Calculus. Applications cover broad areas in automated reasoning, programming language design, semantics, and implementations, and symbolic and algebraic manipulation. The proceedings of the third International Conference on Rewriting Techniques and Applications contain 34 regular papers, covering many diverse aspects of rewriting (including equational logic, decidability questions, term rewriting, congruence-class rewriting, string rewriting, conditional rewriting, graph rewriting, functional and logic programming languages, lazy and parallel implementations, termination issues, compilation techniques, completion procedures, unification and matching algorithms, deductive and inductive theorem proving, Gröbner bases, and program synthesis). It also contains 12 descriptions of implemented equational reasoning systems. Anyone interested in the latest advances in this fast growing area should read this volume.

---

Table of contents :
Term rewriting and universal algebra in historical perspective….Pages 1-1
Characterizations of unification type zero….Pages 2-14
Proof normalization for resolution and paramodulation….Pages 15-28
Complete sets of reductions modulo associativity, commutativity and identity….Pages 29-44
Completion-time optimization of rewrite-time goal solving….Pages 45-58
Computing ground reducibility and inductively complete positions….Pages 59-75
Inductive proofs by specification transformations….Pages 76-91
Narrowing and unification in functional programming —An evaluation mechanism for absolute set abstraction….Pages 92-108
Simulation of Turing machines by a left-linear rewrite rule….Pages 109-120
Higher-order unification with dependent function types….Pages 121-136
An overview of LP, the Larch Prover….Pages 137-151
Graph grammars, a new paradigm for implementing visual languages….Pages 152-166
Termination proofs and the length of derivations….Pages 167-177
Abstract rewriting with concrete operators….Pages 178-186
On how to move mountains ‘associatively and commutatively’….Pages 187-202
Generalized Gröbner bases: Theory and applications. A condensation….Pages 203-221
A local termination property for term rewriting systems….Pages 222-233
An equational logic sampler….Pages 234-262
Modular aspects of properties of term rewriting systems related to normal forms….Pages 263-277
Priority rewriting: Semantics, confluence, and conditionals….Pages 278-291
Negation with logical variables in conditional rewriting….Pages 292-310
Algebraic semantics and complexity of term rewriting systems….Pages 311-325
Optimization by non-deterministic, lazy rewriting….Pages 326-342
Combining matching algorithms: The regular case….Pages 343-358
Restrictions of congruences generated by finite canonical string-rewriting systems….Pages 359-370
Embedding with patterns and associated recursive path ordering….Pages 371-387
Rewriting techniques for program synthesis….Pages 388-403
Transforming strongly sequential rewrite systems with constructors for efficient parallel execution….Pages 404-418
Efficient ground completion….Pages 419-433
Extensions and comparison of simplification orderings….Pages 434-448
Classes of equational programs that compile into efficient machine code….Pages 449-461
Fair termination is decidable for ground systems….Pages 462-476
Termination for the direct sum of left-linear term rewriting systems….Pages 477-491
Conditional rewrite rule systems with built-in arithmetic and induction….Pages 492-512
Consider only general superpositions in completion procedures….Pages 513-527
Solving systems of linear diophantine equations and word equations….Pages 529-532
SbReve2: A term rewriting laboratory with (AC)-unfailing completion….Pages 533-537
THEOPOGLES — An efficient theorem prover based on rewrite-techniques….Pages 538-541
Comtes — An experimental environment for the completion of term rewriting systems….Pages 542-546
Asspegique: An integrated specification environment….Pages 547-547
KBlab: An equational theorem prover for the Macintosh….Pages 548-550
Fast Knuth-Bendix completion: Summary….Pages 551-555
Compilation of ground term rewriting systems and applications (DEMO)….Pages 556-558
An overview of Rewrite Rule Laboratory (RRL)….Pages 559-563
InvX: An automatic function inverter….Pages 564-568
A parallel implementation of rewriting and narrowing….Pages 569-573
Morphocompletion for one-relation monoids….Pages 574-578