A completion procedure for conditional equations

DOI10.1016/S0747-7171(08)80132-0zbMath0724.68053MaRDI QIDQ758211

Harald Ganzinger

Publication date: 1991

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

zbMATH Keywords

completionconditional equationsconditional rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Equational classes, universal algebra in model theory (03C05)

Related Items (10)

Reduction techniques for first-order reasoning ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Order-sorted completion: The many-sorted way ⋮ Efficient deduction in equality Horn logic by Horn-completion ⋮ Specification and proof in membership equational logic ⋮ Proving semantical equivalence of data specifications ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Canonical Ground Horn Theories ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ Deductive and inductive synthesis of equational programs

Cites Work

• Conditional rewrite rules
• Termination of rewriting
• Conditional rewrite rules: Confluence and termination
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Solvable cases of the decision problem
• Proving termination with multiset orderings
• Proof normalization for resolution and paramodulation
• Completion of first-order clauses with equality by strict superposition
• Clausal rewriting
• 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: A completion procedure for conditional equations