Rewriting Techniques and Applications: 7th International Conference, RTA-96, New Brunswick, NJ, USA July 27 - 30, 1996. Proceedings (Lecture Notes in Computer Science, 1103)

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. 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 "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."--PUBLISHER'S WEBSITE