Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
DOI10.1007/s10817-017-9423-7zbMath1468.68302OpenAlexW2753309515WikidataQ123335389 ScholiaQ123335389MaRDI QIDQ670696
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
convex polygonsIsabelle/HOLinteractive theorem provingErdős-Szekeres conjectureSAT-solvinghappy ending problem
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)
Related Items (4)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Formalization and implementation of modern SAT solvers
- Axioms and hulls
- Isabelle/HOL. A proof assistant for higher-order logic
- The Erdős-Szekeres Problem
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Computer solution to the 17-point Erdős-Szekeres problem
- A Compiled Implementation of Normalization by Evaluation
- On Convex Polygons Determined by a Finite Planar Set
- The Erdos-Szekeres problem on points in convex position – a survey
- The Mechanical Verification of a DPLL-Based Satisfiability Solver
- On the Erdős-Szekeres convex polygon problem
- 30 years of research and development around Coq
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Efficient verified (UN)SAT certificate checking
This page was built for publication: Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
