AC-superposition with constraints: No AC-unifiers needed (Q5210796): Difference between revisions

@@ Property / cites work @@
+Completion for rewriting modulo a congruence
@@ Property / cites work: Completion for rewriting modulo a congruence / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Q4264723
@@ Property / cites work: Q4264723 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385532
@@ Property / cites work: Q4385532 / rank @@
+Normal rank
@@ Property / cites work @@
+A technical note on AC-unification. The number of minimal unifiers of the equation \(\alpha x_ 1+ \cdots + \alpha x_ p \doteq _{AC} \beta y_ 1+ \cdots + \beta y_ q\)
+Normal rank
@@ Property / cites work @@
+Completion of a Set of Rules Modulo a Set of Equations
+Normal rank
@@ Property / cites work @@
+Complexity of unification problems with associative-commutative operators
+Normal rank
@@ Property / cites work @@
+Any ground associative-commutative theory has a finite canonical system
+Normal rank
@@ Property / cites work @@
+Q4264721
@@ Property / cites work: Q4264721 / rank @@
+Normal rank
@@ Property / cites work @@
+Complete Sets of Reductions for Some Equational Theories
+Normal rank
@@ Property / cites work @@
+A total AC-compatible ordering based on RPO
@@ Property / cites work: A total AC-compatible ordering based on RPO / rank @@
+Normal rank
@@ Property / cites work @@
+Automated deduction with associative-commutative operators
+Normal rank