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

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