| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Markus Roggenbach, Lutz Schröder, Till Mossakowski |
| Herausgeber: |
Christine Choppy, Didier Bert |
| Titel: |
Specifying real numbers in {CASL} |
| Buch / Sammlungs-Titel: |
Recent Developments in Algebraic Development Techniques, 14th International Workshop, WADT'99 |
| Band: |
1827 |
| Seite(n): |
146 – 161 |
| Serie / Reihe: |
Lecture Notes in Computer Science |
| Erscheinungsjahr: |
2000 |
| Verleger: |
Springer, Berlin |
| Abstract / Kurzbeschreibung: |
We present a weak theory 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. Our theory captures for instance e and pi, 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 and specifications of the real numbers in higher order logic and various set theories.
|
| ISBN: |
3-540-67898-0 |
| Internet: |
http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=1827&spage=146 |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/reals.ps.gz |
| Schlagworte: |
real numbers CASL |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
01. 02. 2006 |
