Specifying real numbers in CASL

摘要

We present a weak theory BASICREAL of the real numbers in the first order specification language CASL. The aim is to provide a datatype for practical purposes, including the central notions and results of basic analysis. BASICREAL captures for instance e and π, as well as the trigonometric and other standard functions. Concepts such as continuity, differentiation and integration are shown to be definable and tractable in this setting; Newton's Method is presented as an example of a numerical application. Finally, we provide a proper connection between the specified datatype BASICREAL and specifications of the real numbers in higher order logic and various set theories.