Verification of Closest Pair of Points Algorithms

DOI10.1007/978-3-030-51054-1_20MaRDI QIDQ5049012zbMATH OpenOpenAlexFDO

Authors 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)

Cites work

• An improved algorithm for finding the closest pair of points
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• An optimized divide-and-conquer algorithm for the closest-pair problem in the planar case
• Automated Deduction in Geometry
• Concrete semantics. With Isabelle/HOL
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Formal study of plane Delaunay triangulation
• Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs
• Formalizing mathematics in higher-order logic: A case study in geometric modelling
• scientific article; zbMATH DE number 3919830 (Why is no real title available?)
• scientific article; zbMATH DE number 3569833 (Why is no real title available?)
• scientific article; zbMATH DE number 1863395 (Why is no real title available?)
• scientific article; zbMATH DE number 1391661 (Why is no real title available?)
• Introduction to algorithms.
• Isabelle/HOL. A proof assistant for higher-order logic
• On the solution of linear recurrence equations
• Proving divide and conquer complexities in Isabelle/HOL
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Verified Root-Balanced Trees

Cited in

(2)

• A note concerning the closest point pair algorithm.
• Rabin's Closest Pair of Points Algorithm

Describes a project that uses

Uses Software

• Isabelle/HOL
• Archive of Formal Proofs

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5049012)