Automated deduction with associative-commutative operators
From MaRDI portal
Publication:1340508
DOI10.1007/BF01270929zbMATH Open0823.68096OpenAlexW2571001698MaRDI QIDQ1340508FDOQ1340508
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
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
- Termination of rewriting systems by polynomial interpretations and its implementation
- Orderings for term-rewriting systems
- Title not available (Why is that?)
- A Unification Algorithm for Associative-Commutative Functions
- Complete Sets of Reductions for Some Equational Theories
- Title not available (Why is that?)
- Proving refutational completeness of theorem-proving strategies
- Title not available (Why is that?)
- Completion of a Set of Rules Modulo a Set of Equations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Completion for rewriting modulo a congruence
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Title not available (Why is that?)
- Using forcing to prove completeness of resolution and paramodulation
- Proving Theorems with the Modification Method
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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 (12)
- Positive deduction modulo regular theories
- Theorem proving modulo associativity
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Title not available (Why is that?)
- 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
- Associative-commutative deduction with constraints
Uses Software
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)
