Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper gives an overview of the formalization of the Harthong-Reeb integer number system (HRω) in the proof-assistant Isabelle. The work builds on an existing mechanization of nonstandard analysis and describes how the basic notions underlying HRω can be recovered and shown to have their expected properties, without the need to introduce any axioms. We also look at the formalization of the well-known Euler method over the new integers and formally prove that the algorithmic approximation produced can be made to be infinitely-close to its continuous counterpart. This enables the discretization of continuous functions and of geometric concepts such as the straight line and ellipse and acts as the starting point for the field of discrete analytical geometry.

Original languageEnglish
Title of host publicationAutomated Deduction in Geometry
Subtitle of host publication8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers
EditorsPascal Schreck, Julien Narboux, Jürgen Richter-Gebert
PublisherSpringer-Verlag GmbH
Pages34-50
Number of pages17
ISBN (Electronic)978-3-642-25070-5
ISBN (Print)978-3-642-25069-9
DOIs
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume6877
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this