Automated deduction with associative-commutative operators
type: Item
instance of: scholarly article
title: Automated deduction with associative-commutative operators
zbMATH Open document ID: 0823.68096
DOI: 10.1007/BF01270929
author: Michaël Rusinowitch
author: Laurent Vigneron
published in: Applicable Algebra in Engineering, Communication and Computing
publication date: 1994-12-14T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 703292
zbMATH Keywords: AC-unification algorithm
describes a project that uses: REVE
describes a project that uses: SbReve2
MaRDI profile type: Publication
cites work: Completion for rewriting modulo a congruence
cites work: Q3696500
cites work: Proving Theorems with the Modification Method
cites work: Termination of rewriting systems by polynomial interpretations and its implementation
cites work: Orderings for term-rewriting systems
cites work: Q3028369
cites work: Proving refutational completeness of theorem-proving strategies
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Q5581665
cites work: Q4139711
cites work: Any ground associative-commutative theory has a finite canonical system
cites work: A general refutational completeness result for an inference procedure based on associative-commutative unification
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Q4279084
cites work: Q5678447
cites work: Using forcing to prove completeness of resolution and paramodulation
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Q4279086
cites work: Q5624683
cites work: A Unification Algorithm for Associative-Commutative Functions
cites work: Q3336737
full work available at URL: https://doi.org/10.1007/bf01270929
OpenAlex ID: W2571001698
Recommended article: Associative-commutative deduction with constraints
Recommended article: Q2757832
Recommended article: Automated Reasoning in Kleene Algebra
Recommended article: Automated Deduction in Ring Theory
Recommended article: Automated deduction for many-valued logics
Recommended article: Q4332419
Recommended article: Automated deduction in equational logic and cubic curves
Recommended article: Q4013071
Recommended article: Automated Deduction in Gödel Logic
Recommended article: Q4941841
description: scientific article; zbMATH DE number 703292