Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Automatic theorem proving in geometry
Prof. Dr. J"urgen Richter-Gebert
ETH Z"urich
Informatik-Kolloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 11 July 97
15:00
-- Not specified --
45 - FB14
HS 001
Saarbrücken
Abstract
In the same way as geometric theorems have been a challenge for the human mind
since centuries, they are now challenging the power of computers (and their
programmers). How can one build up programs that take as input a set of
geometric hypotheses (which describe for instance the position of the heights
in a triangle) and produce a proof for a desired conclusion (for instance the
fact that these heights meet in a point).
After investigating the question `What does it mean to prove a theorem',
we will compare different approaches to automatic theorem proving.
- The logical approach; where one tries to form proofs a la Euclid,
by strict logical deduction that starts from hypotheses and an axiom system.
- The algebraic approach; where the theorems are translated into polynomials,
and wherer the conclusion is derived from the hypotheses by algebraic
operations.
- The randomized approach; where one `just' tries to convince oneself of the
validity of a theorem with arbitrarily high probability.
In paricular, we will see how geometric approaches that date back to the last
since centuries, they are now challenging the power of computers (and their
programmers). How can one build up programs that take as input a set of
geometric hypotheses (which describe for instance the position of the heights
in a triangle) and produce a proof for a desired conclusion (for instance the
fact that these heights meet in a point).
After investigating the question `What does it mean to prove a theorem',
we will compare different approaches to automatic theorem proving.
- The logical approach; where one tries to form proofs a la Euclid,
by strict logical deduction that starts from hypotheses and an axiom system.
- The algebraic approach; where the theorems are translated into polynomials,
and wherer the conclusion is derived from the hypotheses by algebraic
operations.
- The randomized approach; where one `just' tries to convince oneself of the
validity of a theorem with arbitrarily high probability.
In paricular, we will see how geometric approaches that date back to the last
century are helpful to find short and elegant algebraic formulations
for geometric theorems and their proofs.
Contact
--email hidden
passcode not visible
logged in users only
Tags, Category, Keywords and additional notes
Interessenten sind zum Vortrag herzlich eingeladen.
Die Dozenten des Fachbereichs Informatik
Die Dozenten des Fachbereichs Informatik
Uwe Brahm, 04/12/2007 12:39 -- Created document.