Associative-commutative deduction with constraints

DOI10.1007/3-540-58156-1_39zbMath1433.68570OpenAlexW1583508425MaRDI QIDQ5210795

Laurent Vigneron

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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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