Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (Q670696): 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 @@
+DRAT-trim
@@ Property / describes a project that uses: DRAT-trim / 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 @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/Isar
@@ Property / describes a project that uses: Isabelle/Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q123335389
@@ Property / Wikidata QID: Q123335389 / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-017-9423-7
+Normal rank
@@ Property / OpenAlex ID @@
+W2753309515
@@ Property / OpenAlex ID: W2753309515 / rank @@
+Normal rank
@@ Property / cites work @@
+A Compiled Implementation of Normalization by Evaluation
+Normal rank
@@ Property / cites work @@
+Interpretation of Locales in Isabelle: Theories and Proof Contexts
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+On Convex Polygons Determined by a Finite Planar Set
+Normal rank
@@ Property / cites work @@
+Q3653496
@@ Property / cites work: Q3653496 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5759552
@@ Property / cites work: Q5759552 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5302558
@@ Property / cites work: Q5302558 / rank @@
+Normal rank
@@ Property / cites work @@
+years of research and development around Coq
@@ Property / cites work: 30 years of research and development around Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q5628820
@@ Property / cites work: Q5628820 / rank @@
+Normal rank
@@ Property / cites work @@
+Axioms and hulls
@@ Property / cites work: Axioms and hulls / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient verified (UN)SAT certificate checking
@@ Property / cites work: Efficient verified (UN)SAT certificate checking / rank @@
+Normal rank
@@ Property / cites work @@
+Formalization and implementation of modern SAT solvers
+Normal rank
@@ Property / cites work @@
+Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Q6173578
@@ Property / cites work: Q6173578 / rank @@
+Normal rank
@@ Property / cites work @@
+The Erdos-Szekeres problem on points in convex position – a survey
+Normal rank
@@ Property / cites work @@
+The Erdős-Szekeres Problem
@@ Property / cites work: The Erdős-Szekeres Problem / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q4790670
@@ Property / cites work: Q4790670 / rank @@
+Normal rank
@@ Property / cites work @@
+The Mechanical Verification of a DPLL-Based Satisfiability Solver
+Normal rank
@@ Property / cites work @@
+On the Erdős-Szekeres convex polygon problem
@@ Property / cites work: On the Erdős-Szekeres convex polygon problem / rank @@
+Normal rank
@@ Property / cites work @@
+Computer solution to the 17-point Erdős-Szekeres problem
+Normal rank
@@ Property / cites work @@
+Q2848690
@@ Property / cites work: Q2848690 / rank @@
+Normal rank
@@ Property / cites work @@
+DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
+Normal rank