Automated deduction with associative-commutative operators

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

zbMATH Keywords

AC-unification algorithm

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

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

• SbReve2
• REVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Automated deduction with associative-commutative operators