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

Claude Kirchner (eds.)9783540568681, 3540568689

This volume contains the proceedings of RTA-93, the Fifth International Conference on Rewriting Techniques and Applications, held in Montreal, Canada, in June 1993. The volume includes three invited lectures, “Rewrite Techniques in Theorem Proving” (L. Bachmair); “Proving Properties of Typed Lambda Terms: Realizability, Covers, and Sheaves”, (J. Gallier); and “On Some Algorithmic Problems for Groups and Monoids”, (S.J. Adian). It also features full versions of 29 papers selected from 91 submissions, 6 system descriptions, and a list of open problems in the field. The papers cover many topics: term rewriting; termination; graph rewriting; constraint solving; semantic unification, disunification and combination; higher-order logics; and theorem proving, with several papers on distributed theorem proving, theorem proving with constraints and completion.

---

Table of contents :
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