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

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

zbMATH Keywords

convex polygonsIsabelle/HOLinteractive theorem provingErdős-Szekeres conjectureSAT-solvinghappy ending problem

Mathematics Subject Classification ID

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)

Two disjoint 5-holes in point sets ⋮ Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation ⋮ Unnamed Item ⋮ Faradžev Read-type enumeration of non-isomorphic CC systems

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• HOL
• HOL Light
• DRAT-trim

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