Conditional and Typed Rewriting Systems

Conditional rewriting in focus.- A maximal-literal unit strategy for horn clauses.- Extended term rewriting systems.- A proof system for conditional algebraic specifications.- Conditional rewriting logic: Deduction, models and concurrency.- Equivalences of rewrite programs.- On finite representations of infinite sequences of terms.- Infinite terms and infinite rewritings.- Testing confluence of nonterminating rewriting systems.- A survey of ordinal interpretations of type ?0 for termination of rewriting systems.- Meta-rule synthesis from crossed rewrite systems.- An application of automated equational reasoning to many-valued logic.- Completion of first-order clauses with equality by strict superposition.- Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation.- Proof by consistency in conditional equational theories.- Completion procedures as semidecision procedures.- Errata corrige.- Linear completion.- Clausal rewriting.- Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved.- On sufficient completeness of conditional specifications.- FPL : Functional plus logic programming an integration of the FP and Prolog languages.- Confluence of the disjoint union of conditional term rewriting systems.- Implementing term rewriting by graph reduction: Termination of combined systems.- Compiling concurrent rewriting onto the Rewrite Rule Machine.- Design strategies for rewrite rules.- A simplifier for untyped lambda expressions.- Parallel graph rewriting on loosely coupled machine architectures.- Typed equivalence, type assignment, and type containment.- A fixed-point semantics for feature type systems.- Unique-sort order-sorted theories : A description as monad morphisms.- Equational logics (birkhoff's method revisited).- Compatibility of order-sorted rewrite rules.- An universal termination condition for solving goals in equational languages.- Constrained equational deduction.- Higher-order unification, polymorphism, and subsorts.- Second-order unification in the presence of linear shallow algebraic equations.- An inference system for horn clause logic with equality.