Certified Kruskal’s Tree Theorem (Q2938047): Difference between revisions

@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / 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-319-03545-1_12
+Normal rank
@@ Property / OpenAlex ID @@
+W2175970794
@@ Property / OpenAlex ID: W2175970794 / rank @@
+Normal rank
@@ Property / cites work @@
+Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
+Normal rank
@@ Property / cites work @@
+Q5734436
@@ Property / cites work: Q5734436 / rank @@
+Normal rank
@@ Property / cites work @@
+Ordering by Divisibility in Abstract Algebras
@@ Property / cites work: Ordering by Divisibility in Abstract Algebras / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Simple termination of rewrite systems
@@ Property / cites work: Simple termination of rewrite systems / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
+Normal rank
@@ Property / cites work @@
+An intuitionistic proof of Kruskal's theorem
@@ Property / cites work: An intuitionistic proof of Kruskal's theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Stop When You Are Almost-Full
@@ Property / cites work: Stop When You Are Almost-Full / rank @@
+Normal rank
@@ Property / cites work @@
+A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
+Normal rank
@@ Property / cites work @@
+Proving open properties by induction
@@ Property / cites work: Proving open properties by induction / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4246946
@@ Property / cites work: Q4246946 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof pearl: a formal proof of Higman's lemma in ACL2
+Normal rank