Rewriting Techniques and Applications: 5th International Conference, RTA-93 Montreal, Canada, June 16–18, 1993 Proceedings

Front Matter....Pages I-XI
Rewrite techniques in theorem proving....Pages 1-1
Redundancy criteria for constrained completion....Pages 2-16
Bi-rewriting, a term rewriting technique for monotonic order relations....Pages 17-31
A case study of completion modulo distributivity and Abelian groups....Pages 32-46
A semantic approach to order-sorted rewriting....Pages 47-61
Distributing equational theorem proving....Pages 62-76
On the correctness of a distributed memory Gröbner basis algorithm....Pages 77-91
Improving transformation systems for general E -unification....Pages 92-105
Equational and membership constraints for infinite trees....Pages 106-120
Regular path expressions in feature logic....Pages 121-135
Proving properties of typed lambda terms: Realizability, covers, and sheaves....Pages 136-136
Some lambda calculi with categorical sums and products....Pages 137-151
Paths, computations and labels in the λ-calculus....Pages 152-167
Confluence and superdevelopments....Pages 168-182
Relating graph and term rewriting via Böhm models....Pages 183-197
Topics in termination....Pages 198-212
Total termination of term rewriting....Pages 213-227
Simple termination is difficult....Pages 228-242
Optimal normalization in orthogonal term rewriting systems....Pages 243-258
A graph reduction approach to incremental term rewriting....Pages 259-273
Generating tables for bottom-up matching....Pages 274-288
On some algorithmic problems for groups and monoids....Pages 289-300
Combination techniques and decision problems for disunification....Pages 301-315
The negation elimination from syntactic equational formula is decidable....Pages 316-327
Encompassment properties and automata with constraints....Pages 328-342
Recursively defined tree transductions....Pages 343-357
AC complement problems: Satisfiability and negation elimination....Pages 358-373
A precedence-based total AC-compatible ordering....Pages 374-388
Extension of the associative path ordering to a chain of associative commutative symbols....Pages 389-404
Polynomial time termination and constraint satisfaction tests....Pages 405-420
Linear interpretations by counting patterns....Pages 421-433
Some undecidable termination problems for semi-Thue systems....Pages 434-434
Saturation of first-order (constrained) clauses with the Saturate system....Pages 436-440
MERILL: An equational reasoning system in standard ML....Pages 441-445
Reduce the redex → ReDuX....Pages 446-450
Agg — An implementation of algebraic graph rewriting....Pages 451-456
Smaran: A congruence-closure based system for equational computations....Pages 457-461
LAMBDALG: Higher order algebraic specification language....Pages 462-466
More problems in rewriting....Pages 468-487
Back Matter....Pages 488-492