Unnecessary inferences in associative-commutative completion procedures
From MaRDI portal
(Redirected from Publication:3489486)
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
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A Unification Algorithm for Associative-Commutative Functions
- 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
- 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?)
- 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
(7)- Some experiments with a completion theorem prover
- A path ordering for proving termination of AC rewrite systems
- Harald Ganzinger's legacy: contributions to logics and programming
- Redundancy criteria for constrained completion
- Redundancy criteria for constrained completion
- Partial redundancy in saturation
- Reducibility constraints in superposition
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)
