Ernest Schimmerling

Mathematical logic seminar - March 2, 2006

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".