Automated Certification of Implicit Induction Proofs (Q3100200): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+seL4
@@ Property / describes a project that uses: seL4 / 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.1007/978-3-642-25379-9_5
+Normal rank
@@ Property / OpenAlex ID @@
+W2126274963
@@ Property / OpenAlex ID: W2126274963 / rank @@
+Normal rank
@@ Property / cites work @@
+Incorporating decision procedures in implicit induction.
+Normal rank
@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Q4447243
@@ Property / cites work: Q4447243 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Mathematical Induction
@@ Property / cites work: Automated Mathematical Induction / rank @@
+Normal rank
@@ Property / cites work @@
+Certification of Automated Termination Proofs
@@ Property / cites work: Certification of Automated Termination Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q2767010
@@ Property / cites work: Q2767010 / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive proof search modulo
@@ Property / cites work: Inductive proof search modulo / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754095
@@ Property / cites work: Q2754095 / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanical verification of an ideal incremental ABR conformance algorithm
+Normal rank
@@ Property / cites work @@
+A general framework to build contextual cover set induction provers
+Normal rank
@@ Property / cites work @@
+Automated Reasoning with Analytic Tableaux and Related Methods
+Normal rank
@@ Property / cites work @@
+Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
+Normal rank