Automated deduction with associative-commutative operators

DOI10.1007/BF01270929MaRDI QIDQ1340508zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Associative-commutative deduction with constraints
• scientific article; zbMATH DE number 1678379
• Automated Reasoning in Kleene Algebra
• Automated deduction in ring theory
• Automated deduction for many-valued logics
• scientific article; zbMATH DE number 978243
• Automated deduction in equational logic and cubic curves
• scientific article; zbMATH DE number 63734
• Automated deduction in Gödel logic
• Publication:4941841

Cites work

• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 3870641 (Why is no real title available?)
• scientific article; zbMATH DE number 3921960 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 500951 (Why is no real title available?)
• scientific article; zbMATH DE number 500953 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• A Unification Algorithm for Associative-Commutative Functions
• A general refutational completeness result for an inference procedure based on associative-commutative unification
• Any ground associative-commutative theory has a finite canonical system
• Complete Sets of Reductions for Some Equational Theories
• Completion for rewriting modulo a congruence
• Completion of a Set of Rules Modulo a Set of Equations
• Orderings for term-rewriting systems
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• Termination of rewriting systems by polynomial interpretations and its implementation
• Using forcing to prove completeness of resolution and paramodulation

Cited in

(12)

• Associative-commutative deduction with constraints
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Positive deduction modulo regular theories
• Theorem proving modulo associativity
• scientific article; zbMATH DE number 1185498 (Why is no real title available?)
• Associative-Commutative Deducibility Constraints
• Unnecessary inferences in associative-commutative completion procedures
• ELAN from a rewriting logic point of view
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• AC-superposition with constraints: no AC-unifiers needed
• An assertional language for the verification of systems parametric in several dimensions (preliminary results)
• A general refutational completeness result for an inference procedure based on associative-commutative unification

Describes a project that uses

Uses Software

• REVE
• SbReve2

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1340508)