7th international conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996 : proceedings /
Harald Ganzinger (ed.)
xi, 435 pages :
illustrations ;
24 cm
Lecture notes in computer science,
1103
0302-9743 ;
Includes bibliographical references and index
Invited Talk: Rewrite-Based Automated Reasoning: Challenges Ahead / Deepak Kapur -- Fine-Grained Concurrent Completion / Claude Kirchner, Christopher Lynch and Christelle Scharff -- AC-Complete Unification and its Application to Theorem Proving / Alexandre Boudet, Evelyne Contejean and Claude Marche -- Superposition Theorem Proving for Abelian Groups Represented as Integer Modules / Jurgen Stuber -- Symideal Grobner Bases / Manfred Gobel -- Termination of Constructor Systems / Thomas Arts and Jurgen Giesl -- Dummy Elimination in Equational Rewriting / M.C.F. Ferreira -- On Proving Termination by Innermost Termination / Bernhard Gramlich -- A Recursive Path Ordering for Higher-Order Terms in [eta]-Long [beta]-Normal Form / Jean-Pierre Jouannaud and Albert Rubio -- Higher-Order Superposition for Dependent Types / Roberto Virga -- Higher-Order Narrowing with Definitional Trees / Michael Hanus and Christian Prehofer -- Invited Talk: Design of a Proof Assistant / Gerard Huet
0
"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
Algorithms, Congresses
Computer programming, Congresses
Rewriting systems (Computer science), Congresses
base Gröbner
déduction
lambda calcul
Logique
réécriture
réecriture conditionnelle
réécriture graphe
Sémantique
théorie type
unification
005
.
13/1
20
QA267
.
R48
1996
Ganzinger, H., (Harald),1950-
International Conference on Rewriting Techniques and Applications(7th :1996 :, New Brunswick, N.J.)