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

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.

---

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.

---

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.
Content:
Front Matter....Pages -
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
Distributed larch prover (DLP): An experiment in parallelizing a rewrite-rule based prover....Pages 416-419
EPIC: An equational language Abstract machine and supporting tools....Pages 420-423
SPIKE-AC: A system for proofs by induction in Associative-Commutative theories....Pages 424-427
On gaining efficiency in completion-based theorem proving....Pages 428-431
Back Matter....Pages 432-435
....Pages -