Automated deduction with associative-commutative operators
From MaRDI portal
Publication:1340508
DOI10.1007/BF01270929zbMath0823.68096OpenAlexW2571001698MaRDI QIDQ1340508
Michaël Rusinowitch, Laurent Vigneron
Publication date: 14 December 1994
Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf01270929
Related Items (5)
An Assertional Language for the Verification of Systems Parametric in Several Dimensions ⋮ AC-superposition with constraints: No AC-unifiers needed ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II ⋮ ELAN from a rewriting logic point of view
Uses Software
Cites Work
- Termination of rewriting systems by polynomial interpretations and its implementation
- Orderings for term-rewriting systems
- Using forcing to prove completeness of resolution and paramodulation
- A general refutational completeness result for an inference procedure based on associative-commutative unification
- Completion for rewriting modulo a congruence
- Any ground associative-commutative theory has a finite canonical system
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Completion of a Set of Rules Modulo a Set of Equations
- A Unification Algorithm for Associative-Commutative Functions
- Complete Sets of Reductions for Some Equational Theories
- Proving Theorems with the Modification Method
- Proving refutational completeness of theorem-proving strategies
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Automated deduction with associative-commutative operators
