Conditional congruence closure over uninterpreted and interpreted symbols (Q1730315): Difference between revisions

@@ Property / cites work @@
+Variations on the Common Subexpression Problem
@@ Property / cites work: Variations on the Common Subexpression Problem / rank @@
+Normal rank
@@ Property / cites work @@
+An algorithm for reasoning about equality
@@ Property / cites work: An algorithm for reasoning about equality / rank @@
+Normal rank
@@ Property / cites work @@
+Fast Decision Procedures Based on Congruence Closure
+Normal rank
@@ Property / cites work @@
+Implementing contextual rewriting
@@ Property / cites work: Implementing contextual rewriting / rank @@
+Normal rank
@@ Property / cites work @@
+Constraint solving for interpolation
@@ Property / cites work: Constraint solving for interpolation / rank @@
+Normal rank
@@ Property / cites work @@
+Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
+Normal rank
@@ Property / cites work @@
+Linear-time algorithms for testing the satisfiability of propositional horn formulae
+Normal rank
@@ Property / cites work @@
+Shostak's congruence closure as completion
@@ Property / cites work: Shostak's congruence closure as completion / rank @@
+Normal rank
@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiency of a Good But Not Linear Set Union Algorithm
+Normal rank
@@ Property / cites work @@
+An improved equivalence algorithm
@@ Property / cites work: An improved equivalence algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+Q5657644
@@ Property / cites work: Q5657644 / rank @@
+Normal rank
@@ Property / cites work @@
+Fast congruence closure and extensions
@@ Property / cites work: Fast congruence closure and extensions / rank @@
+Normal rank
@@ Property / cites work @@
+Complete Sets of Reductions for Some Equational Theories
+Normal rank
@@ Property / cites work @@
+Q3789100
@@ Property / cites work: Q3789100 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264723
@@ Property / cites work: Q4264723 / rank @@
+Normal rank
@@ Property / cites work @@
+Completion of a Set of Rules Modulo a Set of Equations
+Normal rank
@@ Property / cites work @@
+Q5581665
@@ Property / cites work: Q5581665 / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract congruence closure
@@ Property / cites work: Abstract congruence closure / rank @@
+Normal rank
@@ Property / cites work @@
+Q4036569
@@ Property / cites work: Q4036569 / rank @@
+Normal rank
@@ Property / cites work @@
+Canonical Ground Horn Theories
@@ Property / cites work: Canonical Ground Horn Theories / rank @@
+Normal rank
@@ Property / cites work @@
+On Shostak's decision procedure for combinations of theories
+Normal rank
@@ Property / cites work @@
+Q4518873
@@ Property / cites work: Q4518873 / rank @@
+Normal rank
@@ Property / cites work @@
+Any ground associative-commutative theory has a finite canonical system
+Normal rank
@@ Property / cites work @@
+Q3703293
@@ Property / cites work: Q3703293 / rank @@
+Normal rank
@@ Property / cites work @@
+On interpolation in automated theorem proving
@@ Property / cites work: On interpolation in automated theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+Cover Algorithms and Their Combination
@@ Property / cites work: Cover Algorithms and Their Combination / rank @@
+Normal rank
@@ Property / cites work @@
+Q3338229
@@ Property / cites work: Q3338229 / rank @@
+Normal rank
@@ Property / cites work @@
+New decision algorithms for finitely presented commutative semigroups
+Normal rank