This volume contains the papers preesented at the Third International Workshop on Conditional Term Rewriting Systems, held in Pont- -Mousson, France, July 8-10, 1992. Topics covered include conditional rewriting and its applications to programming languages, specification languages, automated deduction, constrained rewriting, typed rewriting, higher-order rewriting, and graph rewriting. The volume contains 40 papers, including four invited talks: Algebraic semantics of rewriting terms and types, by K. Meinke; Generic induction proofs, by P. Padawitz; Conditional term rewriting and first-order theorem proving, by D. Plaisted; and Decidability of finiteness properties (abstract), by L. Pacholski. The first CTRS workshop was held at the University of Paris in 1987 and the second at Concordia University, Montreal, in 1990. Their proceddings are published as Lecture Notes in Computer Science Volumes 308 and 516 respectively.
Author(s): Karl Meinke (auth.), Michaël Rusinowitch, Jean-Luc Rémy (eds.)
Series: Lecture Notes in Computer Science 656
Edition: 1
Publisher: Springer Berlin Heidelberg
Year: 1993
Language: English
Pages: XIII, 507 p.
Content:
Front Matter....Pages -
Algebraic semantics of rewriting terms and types....Pages 1-20
Context rewriting....Pages 21-35
Explicit cyclic substitutions....Pages 36-50
Simple type inference for term graph rewriting systems....Pages 51-66
Consistency and semantics of equational definitions over predefined algebras....Pages 67-81
Completeness of combinations of conditional constructor systems....Pages 82-96
Collapsed tree rewriting: Completeness, confluence, and modularity....Pages 97-112
Combinations of simplifying conditional term rewriting systems....Pages 113-127
Sufficient conditions for modular termination of conditional term rewriting systems....Pages 128-142
Termination of combined (rewrite and λ-calculus) systems....Pages 143-147
Type removal in term rewriting....Pages 148-154
Termination of term rewriting by interpretation....Pages 155-167
Path orderings for termination of associative-commutative rewriting....Pages 168-174
Generic induction proofs....Pages 175-197
A constructor-based approach for positive/negative-conditional equational specifications....Pages 198-212
Semantics for positive/negative conditional rewrite systems....Pages 213-225
Inductive theorem proving by consistency for first-order clauses....Pages 226-241
Reduction techniques for first-order reasoning....Pages 242-256
Conditional term rewriting and first-order theorem proving....Pages 257-271
Decidability of regularity and related properties of ground normal form languages....Pages 272-286
Computing linearizations using test sets....Pages 287-301
Proving group isomorphism theorems....Pages 302-306
Could orders be captured by term rewriting systems?....Pages 307-314
A categorical formulation for critical-pair/completion procedures....Pages 315-327
Trace rewriting systems....Pages 328-342
A calculus for conditional inductive theorem proving....Pages 343-356
Implementing contextual rewriting....Pages 357-362
Confluence of terminating membership conditional TRS....Pages 363-377
Completeness and confluence of order-sorted term rewriting....Pages 378-392
Completion for constrained term rewriting systems....Pages 393-407
Generalized partial computation using disunification to solve constraints....Pages 408-423
Decidability of finiteness properties....Pages 424-428
Termination proofs of well-moded logic programs via conditional rewrite systems....Pages 429-429
Logic programs with polymorphic types: A condition for static type checking....Pages 430-437
Normalization by leftmost innermost rewriting....Pages 438-447
A strategy to deal with divergent rewrite systems....Pages 448-457
A new approach to general E-unification based on conditional rewriting systems....Pages 458-467
An optimal narrowing strategy for general canonical systems....Pages 468-482
Set-of-support strategy for higher-order logic....Pages 483-497
Back Matter....Pages 498-501
....Pages -
