A completion procedure for conditional equations

DOI10.1016/S0747-7171(08)80132-0MaRDI QIDQ758211zbMATH OpenFDO

Authors Harald Ganzinger

Publication date 1991

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

Full work available at URL https://doi.org/10.1016/S0747-7171(08)80132-0

zbMATH Keywords

completionconditional equationsconditional rewriting

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4090851
• Partial completion of equational theories
• Completion of a Set of Rules Modulo a Set of Equations
• Resolution of equations in algebraic structures. Volume II: Rewriting techniques
• scientific article; zbMATH DE number 4090770

Cites work

• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Clausal rewriting
• Completion of first-order clauses with equality by strict superposition
• Conditional rewrite rules
• Conditional rewrite rules: Confluence and termination
• scientific article; zbMATH DE number 4016182 (Why is no real title available?)
• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 3921957 (Why is no real title available?)
• scientific article; zbMATH DE number 3928346 (Why is no real title available?)
• scientific article; zbMATH DE number 3930372 (Why is no real title available?)
• scientific article; zbMATH DE number 3938563 (Why is no real title available?)
• scientific article; zbMATH DE number 3981150 (Why is no real title available?)
• scientific article; zbMATH DE number 3990847 (Why is no real title available?)
• scientific article; zbMATH DE number 4064978 (Why is no real title available?)
• scientific article; zbMATH DE number 4078788 (Why is no real title available?)
• scientific article; zbMATH DE number 44069 (Why is no real title available?)
• On restrictions of ordered paramodulation with simplification
• Proof normalization for resolution and paramodulation
• Proving termination with multiset orderings
• Solvable cases of the decision problem
• Termination of rewriting

Cited in

(15)

• Order-sorted completion: The many-sorted way
• Efficient deduction in equality Horn logic by Horn-completion
• Deductive and inductive synthesis of equational programs
• Partial completion of equational theories
• Linear and unit-resulting refutations for Horn theories
• Specification and proof in membership equational logic
• scientific article; zbMATH DE number 4078788 (Why is no real title available?)
• scientific article; zbMATH DE number 4090770 (Why is no real title available?)
• scientific article; zbMATH DE number 4090851 (Why is no real title available?)
• Harald Ganzinger's legacy: contributions to logics and programming
• Canonical ground Horn theories
• From search to computation: redundancy criteria and simplification at work
• Equation solving in conditional AC-theories
• Reduction techniques for first-order reasoning
• Proving semantical equivalence of data specifications

This page was built for publication: A completion procedure for conditional equations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q758211)