Shostak's congruence closure as completion

DOI10.1007/3-540-62950-5_59zbMath1379.68196OpenAlexW1567682528MaRDI QIDQ4594216

Deepak Kapur

Publication date: 17 November 2017

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-62950-5_59

Mathematics Subject Classification ID

Related Items (21)

Fast congruence closure and extensions ⋮ Intersection of finitely generated congruences over term algebra ⋮ Term rewriting restricted to ground terms. ⋮ On ground tree transformations and congruences induced by tree automata. ⋮ A rewriting approach to satisfiability procedures. ⋮ Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties ⋮ A pearl on SAT and SMT solving in Prolog ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Canonized Rewriting and Ground AC Completion Modulo Shostak Theories ⋮ <scp>OutsideIn(X)</scp>Modular type inference with local assumptions ⋮ Unnamed Item ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Congruence Closure in Intensional Type Theory ⋮ Model completeness, covers and superposition ⋮ Knuth-Bendix Completion for Non-Symmetric Transitive Relations ⋮ Combination of convex theories: modularity, deduction completeness, and explanation ⋮ Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols ⋮ Restricted ground tree transducers ⋮ Deciding the word problem for ground identities with commutative and extensional symbols ⋮ Deduction, Strategies, and Rewriting

This page was built for publication: Shostak's congruence closure as completion