Any ground associative-commutative theory has a finite canonical system

DOI10.1007/3-540-53904-2_115MaRDI QIDQ5055779zbMATH OpenOpenAlexFDO

Authors Paliath Narendran, Michaël Rusinowitch

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_115

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Recommendations

• Any ground associative-commutative theory has a finite canonical system
• On ground AC-completion
• Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation
• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
• scientific article; zbMATH DE number 1538018

Cites work

• A finite Thue system with decidable word problem and without equivalent finite canonical system
• AC-termination of rewrite systems: a modified Knuth-Bendix ordering
• An Algorithm for the General Petri Net Reachability Problem
• Automated proofs of the Moufang identities in alternative rings
• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Efficient ground completion
• scientific article; zbMATH DE number 4047065 (Why is no real title available?)
• scientific article; zbMATH DE number 4049135 (Why is no real title available?)
• scientific article; zbMATH DE number 4080962 (Why is no real title available?)
• scientific article; zbMATH DE number 18651 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• New decision algorithms for finitely presented commutative semigroups
• Termination of rewriting
• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination orderings for associative-commutative rewriting systems

Cited in

(13)

• 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
• Conditional congruence closure over uninterpreted and interpreted symbols
• Deciding the word problem for ground identities with commutative and extensional symbols
• Proving equational and inductive theorems by completion and embedding techniques
• On ground AC-completion
• A precedence-based total AC-compatible ordering
• Extension of the associative path ordering to a chain of associative commutative symbols
• Linear interpretations by counting patterns
• Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
• Theorem proving modulo associativity
• A total AC-compatible ordering based on RPO

This page was built for publication: Any ground associative-commutative theory has a finite canonical system

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