Induction = I-axiomatization + first-order consistency. (Q1854350): Difference between revisions

@@ Property / describes a project that uses @@
+RRL
@@ Property / describes a project that uses: RRL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Saturate
@@ Property / describes a project that uses: Saturate / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1006/inco.2000.2875
+Normal rank
@@ Property / OpenAlex ID @@
+W2007008828
@@ Property / OpenAlex ID: W2007008828 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4000281
@@ Property / cites work: Q4000281 / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Basic paramodulation
@@ Property / cites work: Basic paramodulation / rank @@
+Normal rank
@@ Property / cites work @@
+Proof by consistency in conditional equational theories
+Normal rank
@@ Property / cites work @@
+Implicit induction in conditional theories
@@ Property / cites work: Implicit induction in conditional theories / rank @@
+Normal rank
@@ Property / cites work @@
+Syntacticness, cycle-syntacticness and shallow theories
+Normal rank
@@ Property / cites work @@
+Ground reducibility is EXPTIME-complete
@@ Property / cites work: Ground reducibility is EXPTIME-complete / rank @@
+Normal rank
@@ Property / cites work @@
+Q4936127
@@ Property / cites work: Q4936127 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4297316
@@ Property / cites work: Q4297316 / rank @@
+Normal rank
@@ Property / cites work @@
+Orderings for term-rewriting systems
@@ Property / cites work: Orderings for term-rewriting systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385532
@@ Property / cites work: Q4385532 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3336735
@@ Property / cites work: Q3336735 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3725540
@@ Property / cites work: Q3725540 / rank @@
+Normal rank
@@ Property / cites work @@
+Proofs by induction in equational theories with constructors
+Normal rank
@@ Property / cites work @@
+Automatic proofs by induction in theories without constructors
+Normal rank
@@ Property / cites work @@
+Proof by consistency
@@ Property / cites work: Proof by consistency / rank @@
+Normal rank
@@ Property / cites work @@
+On ground-confluence of term rewriting systems
@@ Property / cites work: On ground-confluence of term rewriting systems / rank @@
+Normal rank
@@ Property / cites work @@
+On sufficient-completeness and related properties of term rewriting systems
+Normal rank
@@ Property / cites work @@
+Sufficient-completeness, ground-reducibility and their complexity
+Normal rank
@@ Property / cites work @@
+Q3427354
@@ Property / cites work: Q3427354 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
+Normal rank
@@ Property / cites work @@
+Theorem proving with ordering and equality constrained clauses
+Normal rank
@@ Property / cites work @@
+Semantic confluence tests and completion methods
@@ Property / cites work: Semantic confluence tests and completion methods / rank @@
+Normal rank
@@ Property / cites work @@
+Q3477997
@@ Property / cites work: Q3477997 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3348437
@@ Property / cites work: Q3348437 / rank @@
+Normal rank