Consider only general superpositions in completion procedures

DOI10.1007/3-540-51081-8_129MaRDI QIDQ5055743zbMATH OpenOpenAlexFDO

Authors Deepak Kapur, Hantao Zhang

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-51081-8_129

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• scientific article; zbMATH DE number 3928345
• On pot, pans and pudding or how to discover generalised critical pairs
• Critical pair criteria for completion
• scientific article; zbMATH DE number 4090851

Cites work

• A Unification Algorithm for Associative-Commutative Functions
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Complete Sets of Reductions for Some Equational Theories
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Critical pair criteria for completion
• scientific article; zbMATH DE number 3649988 (Why is no real title available?)
• scientific article; zbMATH DE number 3870641 (Why is no real title available?)
• scientific article; zbMATH DE number 3896290 (Why is no real title available?)
• scientific article; zbMATH DE number 3928345 (Why is no real title available?)
• scientific article; zbMATH DE number 3928346 (Why is no real title available?)
• scientific article; zbMATH DE number 3981150 (Why is no real title available?)
• scientific article; zbMATH DE number 4078851 (Why is no real title available?)
• scientific article; zbMATH DE number 41806 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Non-resolution theorem proving
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Problem corner: Reasoning about equality

Cited in

(9)

• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Unnecessary inferences in associative-commutative completion procedures
• A case study of completion modulo distributivity and Abelian groups
• On pot, pans and pudding or how to discover generalised critical pairs
• Complete sets of reductions with constraints
• Redundancy criteria for constrained completion
• Partial redundancy in saturation
• Reducibility constraints in superposition
• Elimination of composite superpositions may cause abortion

This page was built for publication: Consider only general superpositions in completion procedures

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