Contents of the Proceedings of the
7th International Conference on Rewriting Techniques and Applications.
New Brunswick, NJ, USA, July 27-30, 1996.
Lecture Notes in Computer Science, Vol. 1103, Springer Verlag.
Editor: Harald Ganzinger.
Regular Papers
- D. Kapur,
Rewrite-Based Automated Reasoning: Challenges Ahead
(pages 1-2).
- C. Kirchner, C. Lynch and C. Scharff,
Fine-Grained Concurrent Completion
(pages 3-17).
- A. Boudet, E. Contejean and C. Marché,
AC-Complete Unification and its Application to Theorem Proving
(pages 18-32).
- J. Stuber,
Superposition Theorem Proving for Albelian Groups Represented as
Integer Modules
(pages 33-47).
- M. Göbel,
Symideal Gröbner Bases
(pages 48-62).
- T. Arts and J. Giesl,
Termination of Constructor Systems
(pages 63-77).
- M. C. F. Ferreira,
Dummy Elimination in Equational Rewriting
(pages 78-92).
- B. Gramlich,
On Proving Termination by Innermost Termination
(pages 93-107).
- J.-P. Jouannaud and A. Rubio,
A Recursive Path Ordering for Higher-Order Terms in eta-Long
beta-Normal Form
(pages 108-122).
- R. Virga,
Higher-Order Superposition for Dependent Types
(pages 123-137).
- M. Hanus and C. Prehofer,
Higher-Order Narrowing with Definitional Trees
(pages 138-152).
- G. P. Huet,
Design Proof Assistant (Abstract)
(page 153).
- M. Vittek,
A Compiler for Nondeterministic Term Rewriting Systems
(pages 154-167).
- R. Bloo and K. H. Rose,
Combinatory Reduction Systems with Explicit Substitution that
Preserve Strong Nomalisation
(pages 169-183).
- D. Kesner,
Confluence Properties of Extensional and Non-Extensional
lambda-Calculi with Explicit Substitutions (Extended Abstract)
(pages 184-199).
- R. Di Cosmo,
On the Power of Simple Diagrams
(pages 200-214).
- S. Guerrini, S. Martini and A. Masini,
Coherence for Sharing Proof Nets
(pages 215-229).
- M. R. K. Krishna Rao,
Modularity of Termination in Term Graph Rewriting
(pages 230-244).
- B. Gramlich and C.-P. Wirth,
Confluence of Terminating Conditional Rewrite Systems Revisited
(pages 245-259).
- K. Madlener,
Applications of Rewrite Techniques in Monoids and Rings
(Abstract)
(page 260).
- C. Lüth,
Compositional Term Rewriting: An Algebraic Proof of Toyama's
Theorem
(pages 261-275).
- R. Treinen,
The First-Order Theory of One-Step Rewriting is Undecidable
(pages 276-286).
- M. Schmidt-Schauß,
An Algorithm for Distributive Unification
(pages 287-301).
- G. Sénizergues,
On the Termination Problem for One-Rule Semi-Thue System
(pages 302-316).
- R. Curien, Z. Qian and H. Shi,
Efficient Second-Order Matching
(pages 317-331).
- J. Levy,
Linear Second-Order Unification
(pages 332-346).
- R. Fettig and B. Löchner,
Unification of Higher-Order patterns in a Simply Typed
Lambda-Calculus with Finite Products and terminal Type
(pages 347-361).
- F. Jacquemard,
Decidable Approximations of Term Rewriting Systems
(pages 362-376).
- M. Sakai and Y. Toyama,
Semantics and Strong Sequentiality of Priority Term Rewriting
Systems
(pages 377-391).
- V. van Oostrom,
Higher-Order Families
(pages 392-407).
System Descriptions
- F. Voisin,
A New Proof Manager and Graphic Interface for Larch Prover
(pages 408-411).
- R. Bündgen, C. Sinz and J. Walter,
ReDuX 1.5: New Facets of Rewriting
(pages 412-415).
- E. Contejean and C. Marché,
CiME: Completion Modulo E
(pages 416-419).
- M. T. Vandevoorde and D. Kapur,
Distributed Larch Prover (DLP): An Experiment in Parallelizing a
Rewrite-Rule Based Prover
(pages 420-423).
- H. R. Walters and J. F. Th. Kamperman,
EPIC: An Equational Language -Abstract Machine Supporting
Tools-
(pages 424-427).
- N. Berregeb, A. Bouhoula and M. Rusinowitch,
SPIKE-AC: A System for Proofs by Induction in
Associative-Commutative Theories
(pages 428-431).
- T. Hillenbrand, A. Buch and R. Fettig,
On Gaining Efficiency in Completion-Based Theorem Proving
(pages 432-435).