Complete sets of reductions with constraints

DOI10.1007/3-540-52885-7_101MaRDI QIDQ6488546zbMATH OpenFDO

Authors Gerald E. Peterson

Publication date 28 April 2023

Full work available at URL https://doi.org/10.1007/3-540-52885-7_101

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Recommendations

• Complete sets of reductions modulo associativity, commutativity and identity
• Redundancy criteria for constrained completion
• Termination and completion modulo associativity, commutativity and identity
• Complete sets of unifiers and matchers in equational theories
• Redundancy criteria for constrained completion

Cites work

• A Unification Algorithm for Associative-Commutative Functions
• Complete Sets of Reductions for Some Equational Theories
• Complete sets of reductions modulo associativity, commutativity and identity
• Completion of a Set of Rules Modulo a Set of Equations
• Consider only general superpositions in completion procedures
• scientific article; zbMATH DE number 3921957 (Why is no real title available?)
• scientific article; zbMATH DE number 3981150 (Why is no real title available?)
• scientific article; zbMATH DE number 4043234 (Why is no real title available?)
• scientific article; zbMATH DE number 4092758 (Why is no real title available?)
• scientific article; zbMATH DE number 3246263 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• On ground-confluence of term rewriting systems
• On theories with a combinatorial definition of 'equivalence'
• Termination of rewriting
• Ternary Boolean algebra

Cited in

(7)

• Deductive and inductive synthesis of equational programs
• On using ground joinable equations in equational theorem proving
• Redundancy criteria for constrained completion
• Completion for multiple reduction orderings
• Associative-commutative deduction with constraints
• A completion-based method for mixed universal and rigid \(E\)-unification
• Redundancy criteria for constrained completion

This page was built for publication: Complete sets of reductions with constraints

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