Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
DOI10.1007/S10817-017-9423-7zbMATH Open1468.68302OpenAlexW2753309515WikidataQ123335389 ScholiaQ123335389MaRDI QIDQ670696FDOQ670696
Authors: Filip Marić 
Publication date: 20 March 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-017-9423-7
Recommendations
- A partial proof of the Erdős-Szekeres conjecture for hexagons
- scientific article; zbMATH DE number 1786502
- On the Erdős-Szekeres convex polygon problem
- A new proof of the Erdős-Szekeres convex k-gon result
- A generalization of the Erdös-Szekeres convex n-gon theorem.
- On Erdős-Szekeres-type problems for \(k\)-convex point sets
- On Erdős-Szekeres-type problems for \(k\)-convex point sets
- The Erdos-Szekeres problem on points in convex position – a survey
- The \(n\)-point and six-partite point of a convex polygon
convex polygonsinteractive theorem provingIsabelle/HOLSAT-solvinghappy ending problemErdős-Szekeres conjecture
Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Erd?s problems and related topics of discrete geometry (52C10) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computer assisted proofs of proofs-by-exhaustion type (68V05)
Cites Work
- 30 years of research and development around Coq
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- A Compiled Implementation of Normalization by Evaluation
- Title not available (Why is that?)
- Integrating a SAT solver with an LCF-style theorem prover
- A survey of interactive theorem proving
- Formalization and implementation of modern SAT solvers
- Computer solution to the 17-point Erdős-Szekeres problem
- Title not available (Why is that?)
- The Erdős-Szekeres Problem
- The Erdos-Szekeres problem on points in convex position – a survey
- Axioms and hulls
- Title not available (Why is that?)
- Formal proof
- The mechanical verification of a DPLL-based satisfiability solver
- A partial proof of the Erdős-Szekeres conjecture for hexagons
- On Convex Polygons Determined by a Finite Planar Set
- On the Erdős-Szekeres convex polygon problem
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Efficient verified (UN)SAT certificate checking
Cited In (11)
- Computer solution to the 17-point Erdős-Szekeres problem
- A SAT attack on the Erdős-Szekeres conjecture
- Two disjoint 5-holes in point sets
- A partial proof of the Erdős-Szekeres conjecture for hexagons
- A SAT attack on higher dimensional Erdős-Szekeres numbers
- A SAT attack on the Erdős-Szekeres conjecture
- A SAT attack on Erdős-Szekeres numbers in \(\mathbb{R}^d\) and the empty hexagon theorem
- Erdős-Szekeres-type problems in the real projective plane
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
- On the Erdős-Tuza-Valtr conjecture
- Faradžev Read-type enumeration of non-isomorphic CC systems
Uses Software
This page was built for publication: Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q670696)
