Shostak's congruence closure as completion

DOI10.1007/3-540-62950-5_59zbMath1379.68196MaRDI 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

68Q42: Grammars and rewriting systems

Related Items

<scp>OutsideIn(X)</scp>Modular type inference with local assumptions, Unnamed Item, Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties, A pearl on SAT and SMT solving in Prolog, Fast congruence closure and extensions, Combination of convex theories: modularity, deduction completeness, and explanation, 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., Restricted ground tree transducers, Conditional congruence closure over uninterpreted and interpreted symbols, Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes), 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, Model completeness, covers and superposition, Order-Sorted Rewriting and Congruence Closure, Congruence Closure in Intensional Type Theory, Knuth-Bendix Completion for Non-Symmetric Transitive Relations, Deduction, Strategies, and Rewriting, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories