AC-complete unification and its application to theorem proving
From MaRDI portal
Publication:5055849
DOI10.1007/3-540-61464-8_40zbMATH Open1503.68090OpenAlexW1482593535MaRDI QIDQ5055849FDOQ5055849
Authors: Alexandre Boudet, Evelyne Contejean, Claude Marché 
Publication date: 9 December 2022
Published in: Rewriting Techniques and Applications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-61464-8_40
Recommendations
Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
- Title not available (Why is that?)
- A Unification Algorithm for Associative-Commutative Functions
- Complete Sets of Reductions for Some Equational Theories
- Algebraic simplification
- Termination and completion modulo associativity, commutativity and identity
- AC unification through order-sorted AC1 unification
- Normalized rewriting: An alternative to rewriting modulo a set of equations
- Title not available (Why is that?)
- Complete sets of reductions modulo associativity, commutativity and identity
- AC-superposition with constraints: no AC-unifiers needed
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Critical pair criteria for completion
- Combining unification algorithms
- Title not available (Why is that?)
- Completion of a Set of Rules Modulo a Set of Equations
- Associative-commutative unification
- Completion for rewriting modulo a congruence
- Title not available (Why is that?)
- Unification in abelian semigroups
- Associative-commutative deduction with constraints
Cited In (11)
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Path indexing for AC-theories
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- Term Rewriting and Applications
- Superposition theorem proving for abelian groups represented as integer modules
- Superposition theorem proving for abelian groups represented as integer modules
- Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation
- AC-superposition with constraints: no AC-unifiers needed
- Title not available (Why is that?)
- A general refutational completeness result for an inference procedure based on associative-commutative unification
- Verification of the Completeness of Unification Algorithms à la Robinson
This page was built for publication: AC-complete unification and its application to theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055849)
