Associative-commutative deduction with constraints
From MaRDI portal
Publication:5210795
DOI10.1007/3-540-58156-1_39zbMath1433.68570OpenAlexW1583508425MaRDI QIDQ5210795
Publication date: 21 January 2020
Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-58156-1_39
Related Items
On narrowing, refutation proofs and constraints, AC-complete unification and its application to theorem proving, Superposition with completely built-in abelian groups, Theorem proving in cancellative abelian monoids (extended abstract), Superposition theorem proving for abelian groups represented as integer modules, Equational theorem proving modulo, Local simplification, Superposition theorem proving for abelian groups represented as integer modules, Local simplification, Cancellative Abelian monoids and related structures in refutational theorem proving. I
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Theorem-proving with resolution and superposition
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- A general refutational completeness result for an inference procedure based on associative-commutative unification
- Any ground associative-commutative theory has a finite canonical system
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Complete Sets of Reductions for Some Equational Theories
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Proving Theorems with the Modification Method
- Proving refutational completeness of theorem-proving strategies
- A precedence-based total AC-compatible ordering
- Semi-Automated Mathematics