Congruence closure modulo groups

DOI10.46298/LMCS-21(1:20)2025MaRDI QIDQ7016767zbMATH OpenFDO

Authors Dohan Kim

Publication date 6 March 2025

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-21(1:20)2025

Mathematics Subject Classification ID

Applications of universal algebra in computer science (08A70) Applications of logic to group theory (20A15) Word problems, other decision problems, connections with logic and automata (group-theoretic aspects) (20F10) Grammars and rewriting systems (68Q42)

Cites work

• A finite Thue system with decidable word problem and without equivalent finite canonical system
• A Noetherian and confluent rewrite system for idempotent semigroups
• Abstract congruence closure
• Cancellativity in finitely presented semigroups
• Complete Sets of Reductions for Some Equational Theories
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
• Deciding the word problem for ground identities with commutative and extensional symbols
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 3871338 (Why is no real title available?)
• scientific article; zbMATH DE number 3930347 (Why is no real title available?)
• scientific article; zbMATH DE number 3689291 (Why is no real title available?)
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 1241632 (Why is no real title available?)
• scientific article; zbMATH DE number 534859 (Why is no real title available?)
• scientific article; zbMATH DE number 2133330 (Why is no real title available?)
• scientific article; zbMATH DE number 789389 (Why is no real title available?)
• scientific article; zbMATH DE number 7700620 (Why is no real title available?)
• Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• On semigroups with involution
• On termination of the direct sum of term-rewriting systems
• On the Church-Rosser property for the direct sum of term rewriting systems
• On the modularity of termination of term rewriting systems
• Programming up to congruence
• Rewriting
• Satisfiability modulo theories
• Shostak's congruence closure as completion
• Single axioms for groups and abelian groups with various operations
• Term Rewriting and All That
• The Knuth-Bendix Completion Procedure and Thue Systems
• Theorem proving modulo associativity
• Unification theory
• Variations on the Common Subexpression Problem

Cited in

(1)

• An Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems

This page was built for publication: Congruence closure modulo groups

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