Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Multidimensional Binary Search ...


view this post on Zulip Email Gateway (Aug 22 2022 at 20:05):

From: Tobias Nipkow <nipkow@in.tum.de>
Multidimensional Binary Search Trees
Martin Rau

This entry provides a formalization of multidimensional binary trees, also known
as k-d trees. It includes a balanced build algorithm as well as the nearest
neighbor algorithm and the range search algorithm. It is based on the papers
Multidimensional binary search trees used for associative searching and An
Algorithm for Finding Best Matches in Logarithmic Expected Time.

https://www.isa-afp.org/entries/KD_Tree.html

Enjoy!
smime.p7s


Last updated: Nov 21 2024 at 12:39 UTC