Verification of Closest Pair of Points Algorithms

DOI10.1007/978-3-030-51054-1_20OpenAlexW3039044880MaRDI QIDQ5049012

Martin Rau, Tobias Nipkow

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_20

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isabelle/HOL
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• On the solution of linear recurrence equations
• Formalizing mathematics in higher-order logic: A case study in geometric modelling
• Isabelle/HOL. A proof assistant for higher-order logic
• Formal verification of a geometry algorithm: A quest for abstract views and symmetry in coq proofs
• Proving divide and conquer complexities in Isabelle/HOL
• An improved algorithm for finding the closest pair of points
• An optimized divide-and-conquer algorithm for the closest-pair problem in the planar case
• Concrete Semantics
• Verified Root-Balanced Trees
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Automated Deduction in Geometry
• Formal Study of Plane Delaunay Triangulation

This page was built for publication: Verification of Closest Pair of Points Algorithms