Simplifying conditional term rewriting systems: Unification, termination and confluence

DOI10.1016/S0747-7171(87)80010-XzbMath0641.68046MaRDI QIDQ1100891

Stéphane Kaplan

Publication date: 1987

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

theorem provingunificationconfluenceterminationrecursivityconditional term rewriting systems

Mathematics Subject Classification ID

Related Items (26)

Combinations of simplifying conditional term rewriting systems ⋮ Sufficient conditions for modular termination of conditional term rewriting systems ⋮ Semantics for positive/negative conditional rewrite systems ⋮ Confluence of terminating membership conditional TRS ⋮ Conditional rewriting in focus ⋮ A maximal-literal unit strategy for horn clauses ⋮ Extended term rewriting systems ⋮ Proof by consistency in conditional equational theories ⋮ On sufficient completeness of conditional specifications ⋮ Confluence of the disjoint union of conditional term rewriting systems ⋮ An universal termination condition for solving goals in equational languages ⋮ Completeness results for basic narrowing ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Reasoning with conditional axioms ⋮ Higher order conditional rewriting and narrowing ⋮ Conditional semi-Thue systems for presenting monoids ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ Sufficient completeness verification for conditional and constrained TRS ⋮ A rationale for conditional equational programming ⋮ Canonical Ground Horn Theories ⋮ Applications and extensions of context-sensitive rewriting ⋮ Conditional narrowing modulo a set of equations ⋮ On word problems in Horn theories ⋮ Operational termination of conditional term rewriting systems ⋮ Deductive and inductive synthesis of equational programs ⋮ Proving termination of (conditional) rewrite systems. A semantic approach

Uses Software

• REVE

Cites Work

• Proofs by induction in equational theories with constructors
• Conditional rewrite rules
• Algebraic specifications of computable and semicomputable data types
• Conditional rewrite rules: Confluence and termination
• Computing in systems described by equations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Simplifying conditional term rewriting systems: Unification, termination and confluence