7th RTA 1996: New Brunswick, NJ, USA
- Harald Ganzinger:
Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings. Lecture Notes in Computer Science 1103, Springer 1996, ISBN 3-540-61464-8
Regular Papers
- Alexandre Boudet, Evelyne Contejean, Claude Marché:
AC-Complete Unification and its Application to Theorem Proving. 18-32 - Jürgen Stuber:
Superposition Theorem Proving for Albelian Groups Represented as Integer Modules. 33-47 - Jean-Pierre Jouannaud, Albert Rubio:
A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form. 108-122 - Roel Bloo, Kristoffer Høgsbro Rose:
Combinatory Reduction Systems with Explicit Substitution that Preserve Strong Nomalisation. 169-183 - Delia Kesner:
Confluence Properties of Extensional and Non-Extensional lambda-Calculi with Explicit Substitutions (Extended Abstract). 184-199 - Bernhard Gramlich, Claus-Peter Wirth:
Confluence of Terminating Conditional Rewrite Systems Revisited. 245-259 - Roland Fettig, Bernd Löchner:
Unification of Higher-Order patterns in a Simply Typed Lambda-Calculus with Finite Products and terminal Type. 347-361 - Masahiko Sakai, Yoshihito Toyama:
Semantics and Strong Sequentiality of Priority Term Rewriting Systems. 377-391
System Descriptions
- Mark T. Vandevoorde, Deepak Kapur:
Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover. 420-423 - H. R. Walters, J. F. Th. Kamperman:
EPIC: An Equational Language -Abstract Machine Supporting Tools-. 424-427 - Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch:
SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories. 428-431 - Thomas Hillenbrand, Arnim Buch, Roland Fettig:
On Gaining Efficiency in Completion-Based Theorem Proving. 432-435