Automated deduction with associative-commutative operators (Q1340508): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Completion for rewriting modulo a congruence
@@ Property / cites work: Completion for rewriting modulo a congruence / rank @@
+Normal rank
@@ Property / cites work @@
+Q3696500
@@ Property / cites work: Q3696500 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Theorems with the Modification Method
@@ Property / cites work: Proving Theorems with the Modification Method / rank @@
+Normal rank
@@ Property / cites work @@
+Termination of rewriting systems by polynomial interpretations and its implementation
+Normal rank
@@ Property / cites work @@
+Orderings for term-rewriting systems
@@ Property / cites work: Orderings for term-rewriting systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q3028369
@@ Property / cites work: Q3028369 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving refutational completeness of theorem-proving strategies
+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 @@
+Q4139711
@@ Property / cites work: Q4139711 / rank @@
+Normal rank
@@ Property / cites work @@
+Any ground associative-commutative theory has a finite canonical system
+Normal rank
@@ Property / cites work @@
+A general refutational completeness result for an inference procedure based on associative-commutative unification
+Normal rank
@@ Property / cites work @@
+A Technique for Establishing Completeness Results in Theorem Proving with Equality
+Normal rank
@@ Property / cites work @@
+Q4279084
@@ Property / cites work: Q4279084 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5678447
@@ Property / cites work: Q5678447 / rank @@
+Normal rank
@@ Property / cites work @@
+Using forcing to prove completeness of resolution and paramodulation
+Normal rank
@@ Property / cites work @@
+Complete Sets of Reductions for Some Equational Theories
+Normal rank
@@ Property / cites work @@
+Q4279086
@@ Property / cites work: Q4279086 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5624683
@@ Property / cites work: Q5624683 / rank @@
+Normal rank
@@ Property / cites work @@
+A Unification Algorithm for Associative-Commutative Functions
+Normal rank
@@ Property / cites work @@
+Q3336737
@@ Property / cites work: Q3336737 / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/bf01270929
+Normal rank
@@ Property / OpenAlex ID @@
+W2571001698
@@ Property / OpenAlex ID: W2571001698 / rank @@
+Normal rank