Unnecessary inferences in associative-commutative completion procedures

DOI10.1007/BF02090774MaRDI QIDQ3489486zbMATHOpenAlexFDO

Authors Deepak Kapur, Hantao 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

superpositionautomated reasoningcompletion procedureJacobson's theorem

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Consider only general superpositions in completion procedures
• A general refutational completeness result for an inference procedure based on associative-commutative unification
• Some experiments with a completion theorem prover
• Automated deduction with associative-commutative operators

Cites work

• 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 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 41806 (Why is no real title available?)
• scientific article; zbMATH DE number 3445421 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3330761 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Unification Algorithm for Associative-Commutative Functions
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
• Complete Sets of Reductions for Some Equational Theories
• Complexity of matching problems
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Non-resolution theorem proving
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Structure theory for algebraic algebras of bounded degree

Cited in

(5)

• Redundancy criteria for constrained completion
• Redundancy criteria for constrained completion
• Some experiments with a completion theorem prover
• Harald Ganzinger's legacy: contributions to logics and programming
• A path ordering for proving termination of AC rewrite systems

Describes a project that uses

Uses Software

• RRL

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

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