|
On Friday 28th October 2005 the Brouwer Institute in Nijmegen will organise a one-day lecture series on Constructive interactive mathematics. This is a pre-opening of the Diamant lecture series.
The program is as follows:
The workshop will be held in the science building at the campus of the Radboud University.
To get to the campus by public transport take the train from Nijmegen station to Nijmegen Heyendaal. The train trip will take 3 minutes. From the train station the walk to the location takes another ten minutes.
There are also bus lines going to the campus. The buses that run through the Heyendaalseweg are lines 1 (direction Molenhoek) and 11 (direction Brakkenstein).
The event will take place in lecture room HG00.304. This is in the ‘new' Huijgens building, near the main entrance.
Please register for the lunch before 21 October.
Many years ago as an application of Domain Theory I tried to to define ‘free' semigroups with infinite words. Much later I realized that an equivalent and better approach was to use profinite structures, about which there are many results in the literature. The talk will cover the background and basic constructions. An apparently unsolved problem is how to describe the free profinite monoid on two generators. Some preliminary results will be given in hopes that someone else will provide final answers.
This talk is an introduction to formalization of mathematics and decision procedures. The current state of the art in formalization of mathematics will be presented. After that we will argue that \"decision procedures\" (which are algorithms that each solve a specific class of mathematical problems) is the most important technology to make formalization of mathematics more practical than it is today. An overview of the most important currently available decision procedures will then be given.
We give a very brief outline of the skeleton of the proof as given by Ribet, Wiles and others for Fermat's Last Theorem. We subsequently discuss several aspects of the question whether this proof can (or should, or will, or must) be formalized and verified by computer, and how to contribute to this aim.
The problem of determining the validity of boolean combinations of equalities and inequalities between real-valued expressions is important not only for formal verification of mathematical proofs, but, more generally, for any application which depends on such properties of the real numbers.
Alfred Tarski's proof that the theory of real numbers as an ordered field admits quantifier-elimination is a striking and powerful response to this problem. But decision procedures for real closed fields can be inefficient, and, more importantly, are not extendable.
In this talk, I will discuss ideas for obtaining heuristic procedures for the reals by combining \"local\" decision procedures for fragments. This framework poses interesting theoretical problems, and I will present decidability and undecidability results. I will also discuss ways in which the theoretical results bear on pragmatic issues related to implementation.
(Joint work with Harvey Friedman.)
page maintained by Bas
