Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
From MaRDI portal
(Redirected from Publication:670696)
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)
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
Cites work
- scientific article; zbMATH DE number 1863395 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 3354154 (Why is no real title available?)
- scientific article; zbMATH DE number 3019031 (Why is no real title available?)
- 30 years of research and development around Coq
- A Compiled Implementation of Normalization by Evaluation
- A partial proof of the Erdős-Szekeres conjecture for hexagons
- A survey of interactive theorem proving
- Axioms and hulls
- Computer solution to the 17-point Erdős-Szekeres problem
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Efficient verified (UN)SAT certificate checking
- Formal proof
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Formalization and implementation of modern SAT solvers
- Integrating a SAT solver with an LCF-style theorem prover
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Isabelle/HOL. A proof assistant for higher-order logic
- On Convex Polygons Determined by a Finite Planar Set
- On the Erdős-Szekeres convex polygon problem
- The Erdos-Szekeres problem on points in convex position – a survey
- The Erdős-Szekeres Problem
- The mechanical verification of a DPLL-based satisfiability solver
Cited in
(11)- Two disjoint 5-holes in point sets
- On the Erdős-Tuza-Valtr conjecture
- A partial proof of the Erdős-Szekeres conjecture for hexagons
- A SAT attack on higher dimensional Erdős-Szekeres numbers
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
- Faradžev Read-type enumeration of non-isomorphic CC systems
- A SAT attack on the Erdős-Szekeres conjecture
- Computer solution to the 17-point Erdős-Szekeres problem
- Erdős-Szekeres-type problems in the real projective plane
- 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
Describes a project that uses
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)
