The workshop will be held at the campus of the Radboud University Nijmegen
The workshop will be held on 6th of October.
|13:00-14:00||Helmut Schwichtenberg)||Simultaneous inductive/coinductive definition of continuous functions|
|14:00-15:00||Norbert Mueller)||Enhancing imperative exact real arithmetic with functions and logic|
|15:30-16:30||Russell O'Connor||How to Understand What Classical Mathematicians Say|
|16:30-17:30||John Harrison)||Decidability and undecidability in theories of real vector spaces|
How to Understand What Classical Mathematicians Say
Usually people consider constructive mathematics as a restriction of classical mathematics where the law of the excluded middle is disallowed. However, I believe that constructive mathematics is better as an extension of classical mathematics which adds constructive existential quantifier and a constructive function space.
In my talk will cover
Enhancing imperative exact real arithmetic with functions and logic
In the near past, there have been many approaches to `implement' constructive analysis, many of them with the use of functional programmig languages. In this paper we present a similar approach based on the iRRAM-package which has been acknowledged as a fast package for exact real arithmetic in C++. A major concern here is the reduction of space requirements for computations with real numbers.
Simultaneous inductive/coinductive definition of continuous functions
When extracting computational content from proofs in constructive analysis it can be helpful to use simultaneous inductive/coinductive definitons of the real numbers and of (uniformly) continuous real functions. The talk reports on an attempt to design the underlying theory, based on recent work of Ulrich Berger.
Decidability and undecidability in theories of real vector spaces
The known decidability of various elementary theories of real numbers
leads to practical decision procedures that are genuinely useful in
formal proofs. Linear real arithmetic is a staple of verification
systems, and recently there has been increasing interest in the
automation of nonlinear arithmetic via various techniques (quantifier
elimination, sum-of-squares decomposition or more heuristic means).
For many purposes, particularly in geometry, it's natural to wonder whether these results can be extended to analogous theories of real vector spaces, formulated in a 2-sorted first-order language with a sort for vectors and another for real numbers. In joint work, Solovay, Arthan and the speaker have systematically surveyed various theories of this kind. It turns out that the theories of vector spaces and inner product spaces are decidable and even admit quantifier elimination in a suitably expanded language, whereas similar-looking theories of normed spaces are spectacularly undecidable, at least as difficult as second-order arithmetic. The universal "linear" theory of normed spaces, however, is fairly efficiently decidable, and a decision procedure for this theory has been found to be very useful.
Herman Geuvers Nicole Messink Bas Spitters.
Please contact Nicole Messink for practical matters.
Most of you will be arriving at Amsterdam Schiphol airport. The easiest way to get to Nijmegen from there is by train. The train station is under the airport. Just check the screens.
The train trip is 1 hour and 30 - 45 minutes.
There is a train planner on the web.
We have good experiences with:
Bisschop Hamerstraat 14
6511 NB Nijmegen
Tel.: +31 (0)24 - 323 35 94
Fax: +31 (0)24 - 323 31 76
Slightly more expensive is:
6511 XR Nijmegen
Tel.: +31 (0)24 - 360 49 70
Fax: +31 (0)24 - 360 71 77
There also is a web page with alternative accomodation.
The workshop will be held at
It is located at lecture room GN2.
In case you enjoy walking the campus is 30 minutes walk from the city
There is a bus going to the campus. The buses that run through the Heyendaalseweg are lines 1 (direction Molenhoek) and 11 (direction Brakkenstein), 10 (Heyendael Shuttle), 3,4 (Wijchen via Noord/Zuid) all stop outside the "Bloedbank" opposite our building.
page maintained by Bas