Unnecessary inferences in associative-commutative completion procedures

DOI10.1007/BF02090774zbMath0707.68071OpenAlexW2049670190MaRDI QIDQ3489486

Deepak Kapur, Han-Tao Zhang

Publication date: 1990

Published in: Mathematical Systems Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf02090774

zbMATH Keywords

automated reasoningsuperpositioncompletion procedureJacobson's theorem

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (5)

A path ordering for proving termination of AC rewrite systems ⋮ Some experiments with a completion theorem prover ⋮ Redundancy criteria for constrained completion ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Redundancy criteria for constrained completion

Uses Software

• RRL

Cites Work

• Complexity of matching problems
• Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Non-resolution theorem proving
• Structure theory for algebraic algebras of bounded degree
• 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
• Unnamed Item

This page was built for publication: Unnecessary inferences in associative-commutative completion procedures