Rewriting Techniques and Applications: 7th International Conference, RTA-96 New Brunswick, NJ, USA, July 27–30, 1996 Proceedings

Deepak Kapur (auth.), Harald Ganzinger (eds.)3540614648, 9783540614647

This book constitutes the refereed proceedings of the 7th International Conference on Rewriting Techniques and Applications, RTA-96, held in New Brunswick, NJ, USA, in July 1996.
The 27 revised full papers presented in this volume were selected from a total of 84 submissions, also included are six system descriptions and abstracts of three invited papers. The topics covered include analysis of term rewriting systems, string and graph rewriting, rewrite-based theorem proving, conditional term rewriting, higher-order rewriting, unification, symbolic and algebraic computation, and efficient implementation of rewriting on sequential and parallel machines.

---

Table of contents :
Rewrite-based automated reasoning: Challenges ahead….Pages 1-2
Fine-grained concurrent completion….Pages 3-17
AC-complete unification and its application to theorem proving….Pages 18-32
Superposition theorem proving for abelian groups represented as integer modules….Pages 33-47
Symideal Gröbner bases….Pages 48-62
Termination of constructor systems….Pages 63-77
Dummy elimination in equational rewriting….Pages 78-92
On proving termination by innermost termination….Pages 93-107
A recursive path ordering for higher-order terms in η-long β-normal form….Pages 108-122
Higher-order superposition for dependent types….Pages 123-137
Higher-order narrowing with definitional trees….Pages 138-152
Design of a proof assistant….Pages 153-153
A compiler for nondeterministic term rewriting systems….Pages 154-168
Combinatory reduction systems with explicit substitution that preserve strong normalisation….Pages 169-183
Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)….Pages 184-199
On the power of simple diagrams….Pages 200-214
Coherence for sharing proof nets….Pages 215-229
Modularity of termination in term graph rewriting….Pages 230-244
Confluence of terminating conditional rewrite systems revisited….Pages 245-259
Applications of rewrite techniques in monoids and rings….Pages 260-260
Compositional term rewriting: An algebraic proof of Toyama’s theorem….Pages 261-275
The first-order theory of one-step rewriting is undecidable….Pages 276-286
An algorithm for distributive unification….Pages 287-301
On the termination problem for one-rule semi-Thue system….Pages 302-316
Efficient second-order matching….Pages 317-331
Linear second-order unification….Pages 332-346
Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type….Pages 347-361
Decidable approximations of term rewriting systems….Pages 362-376
Semantics and strong sequentially of priority term rewriting systems….Pages 377-391
Higher-order families….Pages 392-407
A new proof manager and graphic interface for the larch prover….Pages 408-411
ReDuX 1.5: New facets of rewriting….Pages 412-415
C i ME: Complet i on modulo E ….Pages 416-419
Distributed larch prover (DLP): An experiment in parallelizing a rewrite-rule based prover….Pages 420-423
EPIC: An equational language Abstract machine and supporting tools….Pages 424-427
SPIKE-AC: A system for proofs by induction in Associative-Commutative theories….Pages 428-431
On gaining efficiency in completion-based theorem proving….Pages 432-435