7. RTA 1996: New Brunswick, NJ, USA

Regular Papers

• Deepak Kapur:
  Rewrite-Based Automated Reasoning: Challenges Ahead. 1-2
  
• Claude Kirchner, Christopher Lynch, Christelle Scharff:
  Fine-Grained Concurrent Completion. 3-17
  
• 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
  
• Manfred Göbel:
  Symideal Gröbner Bases. 48-62
  
• Thomas Arts, Jürgen Giesl:
  Termination of Constructor Systems. 63-77
  
• Maria C. F. Ferreira:
  Dummy Elimination in Equational Rewriting. 78-92
  
• Bernhard Gramlich:
  On Proving Termination by Innermost Termination. 93-107
  
• Jean-Pierre Jouannaud, Albert Rubio:
  A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form. 108-122
  
• Roberto Virga:
  Higher-Order Superposition for Dependent Types. 123-137
  
• Michael Hanus, Christian Prehofer:
  Higher-Order Narrowing with Definitional Trees. 138-152
  
• Gérard P. Huet:
  Design Proof Assistant (Abstract). 153
  
• Marian Vittek:
  A Compiler for Nondeterministic Term Rewriting Systems. 154-167
  
• 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
  
• Roberto Di Cosmo:
  On the Power of Simple Diagrams. 200-214
  
• Stefano Guerrini, Simone Martini, Andrea Masini:
  Coherence for Sharing Proof Nets. 215-229
  
• M. R. K. Krishna Rao:
  Modularity of Termination in Term Graph Rewriting. 230-244
  
• Bernhard Gramlich, Claus-Peter Wirth:
  Confluence of Terminating Conditional Rewrite Systems Revisited. 245-259
  
• Klaus Madlener:
  Applications of Rewrite Techniques in Monoids and Rings (Abstract). 260
  
• Christoph Lüth:
  Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem. 261-275
  
• Ralf Treinen:
  The First-Order Theory of One-Step Rewriting is Undecidable. 276-286
  
• Manfred Schmidt-Schauß:
  An Algorithm for Distributive Unification. 287-301
  
• Géraud Sénizergues:
  On the Termination Problem for One-Rule Semi-Thue System. 302-316
  
• Régis Curien, Zhenyu Qian, Hui Shi:
  Efficient Second-Order Matching. 317-331
  
• Jordi Levy:
  Linear Second-Order Unification. 332-346
  
• Roland Fettig, Bernd Löchner:
  Unification of Higher-Order patterns in a Simply Typed Lambda-Calculus with Finite Products and terminal Type. 347-361
  
• Florent Jacquemard:
  Decidable Approximations of Term Rewriting Systems. 362-376
  
• Masahiko Sakai, Yoshihito Toyama:
  Semantics and Strong Sequentiality of Priority Term Rewriting Systems. 377-391
  
• Vincent van Oostrom:
  Higher-Order Families. 392-407
  

System Descriptions

• Frédéric Voisin:
  A New Proof Manager and Graphic Interface for Larch Prover. 408-411
  
• Reinhard Bündgen, Carsten Sinz, Jochen Walter:
  ReDuX 1.5: New Facets of Rewriting. 412-415
  
• Evelyne Contejean, Claude Marché:
  CiME: Completion Modulo E. 416-419
  
• 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