Rewriting Techniques And Applications: 5th International Conference, Rta-93, Montreal, Canada, June 16-18, 1993. Proceedings (lecture Notes In Computer Science)

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. 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 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), together with 29 selected papers, 6 system descriptions, and a list of open problems in the field. The papers covermany 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 Claude Kirchner, Ed. Includes Bibliographical References And Index.