On ground AC-completion

DOI10.1007/3-540-53904-2_114MaRDI QIDQ5055778zbMATH OpenOpenAlexFDO

Authors 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-53904-2_114

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Word problems, etc. in computability and recursion theory (03D40) Grammars and rewriting systems (68Q42)

Recommendations

• Any ground associative-commutative theory has a finite canonical system
• Any ground associative-commutative theory has a finite canonical system
• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
• On how to move mountains ‘associatively and commutatively’
• Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation

Cites work

• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• scientific article; zbMATH DE number 3301426 (Why is no real title available?)
• scientific article; zbMATH DE number 3045417 (Why is no real title available?)
• On ground AC-completion
• Ordering by Divisibility in Abstract Algebras
• Recursive unsolvability of a problem of Thue

Cited in

(17)

• Termination and completion modulo associativity, commutativity and identity
• Decidability and complexity analysis by basic paramodulation
• Buchberger's algorithm: The term rewriter's point of view
• Any ground associative-commutative theory has a finite canonical system
• The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable.
• On using ground joinable equations in equational theorem proving
• Deciding the word problem for ground identities with commutative and extensional symbols
• Outermost ground termination
• TERM REWRITE RULES FOR FINITE FIELDS
• THE WORD PROBLEM OF ACD-GROUND THEORIES IS UNDECIDABLE
• Complete sets of reductions modulo associativity, commutativity and identity
• On how to move mountains ‘associatively and commutatively’
• On ground AC-completion
• Any ground associative-commutative theory has a finite canonical system
• AC completion with termination tools
• Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
• A total AC-compatible ordering based on RPO

This page was built for publication: On ground AC-completion

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