Associative-commutative deduction with constraints
From MaRDI portal
Publication:5210795
DOI10.1007/3-540-58156-1_39zbMATH Open1433.68570OpenAlexW1583508425MaRDI QIDQ5210795FDOQ5210795
Authors: 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
Recommendations
- Automated deduction with associative-commutative operators
- Termination and completion modulo associativity, commutativity and identity
- Paramodulation with built-in AC-theories and symbolic constraints
- AC-superposition with constraints: no AC-unifiers needed
- A general refutational completeness result for an inference procedure based on associative-commutative unification
Cites Work
- Complete Sets of Reductions for Some Equational Theories
- Proving refutational completeness of theorem-proving strategies
- Title not available (Why is that?)
- Title not available (Why is that?)
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Theorem-proving with resolution and superposition
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Ordered rewriting and confluence
- Title not available (Why is that?)
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Title not available (Why is that?)
- Title not available (Why is that?)
- A precedence-based total AC-compatible ordering
- Complete sets of reductions with constraints
- On restrictions of ordered paramodulation with simplification
- Proving Theorems with the Modification Method
- Semi-Automated Mathematics
- A general refutational completeness result for an inference procedure based on associative-commutative unification
- Any ground associative-commutative theory has a finite canonical system
- Title not available (Why is that?)
Cited In (16)
- Positive deduction modulo regular theories
- Theorem proving modulo associativity
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Local simplification
- Theorem proving in cancellative abelian monoids (extended abstract)
- Equational theorem proving modulo
- Local simplification
- Superposition theorem proving for abelian groups represented as integer modules
- Superposition with completely built-in abelian groups
- Associative-Commutative Deducibility Constraints
- Superposition theorem proving for abelian groups represented as integer modules
- AC-superposition with constraints: no AC-unifiers needed
- Automated deduction with associative-commutative operators
- Constrained equational deduction
- AC-complete unification and its application to theorem proving
- On narrowing, refutation proofs and constraints
This page was built for publication: Associative-commutative deduction with constraints
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5210795)
