| Time: | 12 - 1:20 p.m. |
| Room: |
Dougherty Hall 1209
|
| Speaker: | Wolfgang Windsteiger Johannes Kepler University Linz |
| Title: |
Computer-supported proving in ZF set theory with the Theorema
system
|
| Abstract: |
We present the mathematical assistant system "Theorema", and therein focus on the set theory prover for ZF. We
will give a brief overview on the entire system, how proof search is organized, and how set theory proving is integrated
into this framework. Moreover, we will describe precisely the language constructs from ZF that are supported by the
prover. An emphasis will be put on the combination of "proving, computing, and solving" as a proof search technique. The
talk will give an overview over the main capabilities of the system (and the set theory prover in particular!) and will
mostly feature live demos of example proofs using the set theory prover.
Theorema designed and directed by Bruno Buchberger at RISC Linz, Austria.
In contrast to the lecture on Feb 20, which tried to give an overview over the entire Theorema system philosophy, this
talk will concentrate on proving inside Theorema, how proof search is setup in the system and within the set theory
prover, and it will show much more examples of automated proofs and little to nothing about "computation".
|