Consider only general superpositions in completion procedures

DOI10.1007/3-540-51081-8_129zbMath1503.68171OpenAlexW1511704268MaRDI QIDQ5055743

Deepak Kapur, Han-Tao 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)

Related Items (2)

A case study of completion modulo distributivity and Abelian groups ⋮ Redundancy criteria for constrained completion

Cites Work

• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Critical pair criteria for completion
• Non-resolution theorem proving
• Problem corner: Reasoning about equality
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• Complete Sets of Reductions for Some Equational Theories
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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