Rewriting Techniques and Applications: 4th International Conference, RTA-91 Como, Italy, April 10–12, 1991 Proceedings

Transfinite reductions in orthogonal term rewriting systems....Pages 1-12
Redex capturing in term graph rewriting (concise version)....Pages 13-24
Rewriting, and equational unification: the higher-order cases....Pages 25-36
Adding algebraic rewriting to the untyped lambda calculus (extended abstract)....Pages 37-48
Incremental termination proofs and the length of derivations....Pages 49-61
Time bounded rewrite systems and termination proofs by generalized embedding....Pages 62-73
Detecting redundant narrowing derivations by the LSE-SL reducibility test....Pages 74-85
Unification, weak unification, upper bound, lower bound, and generalization problems....Pages 86-97
AC unification through order-sorted AC1 unification....Pages 98-111
Narrowing directed by a graph of terms....Pages 112-123
Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification....Pages 124-135
Undecidable properties of syntactic theories....Pages 136-149
Goal directed strategies for paramodulation....Pages 150-161
Minimal solutions of linear diophantine systems : bounds and algorithms....Pages 162-173
Proofs in parameterized specifications....Pages 174-187
Completeness of combinations of constructor systems....Pages 188-199
Modular higher-order E -unification....Pages 200-214
On confluence for weakly normalizing systems....Pages 215-225
Program transformation and rewriting....Pages 226-239
An efficient representation of arithmetic for term rewriting....Pages 240-251
Query optimization using rewrite rules....Pages 252-263
Boolean algebra admits no convergent term rewriting system....Pages 264-274
Decidability of confluence and termination of monadic term rewriting systems....Pages 275-286
Bottom-up tree pushdown automata and rewrite systems....Pages 287-298
On relationship between term rewriting systems and regular tree languages....Pages 299-311
The equivalence of boundary and confluent graph grammars on graph languages of bounded degree....Pages 312-322
Left-to-right tree pattern matching....Pages 323-334
Incremental techniques for efficient normalization of nonlinear rewrite systems....Pages 335-347
On fairness of completion-based theorem proving strategies....Pages 348-360
Proving equational and inductive theorems by completion and embedding techniques....Pages 361-373
Divergence phenomena during completion....Pages 374-385
Simulating Buchberger's algorithm by Knuth-Bendix completion....Pages 386-397
On proving properties of completion strategies....Pages 398-410
On ground AC-completion....Pages 411-422
Any ground associative-commutative theory has a finite canonical system....Pages 423-434
A narrowing-based theorem prover....Pages 435-436
ANIGRAF: An interactive system for the animation of graph rewriting systems with priorities....Pages 437-438
Emmy: A refutational theorem prover for first-order logic with equations....Pages 439-441
The tecton proof system....Pages 442-444
Open problems in rewriting....Pages 445-456