author = {W. Windsteiger},
title = {{Computer-supported Proving in ZF Set Theory with the Theorema System}},
language = {english},
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 is 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". },
year = {2006},
month = {March 2},
note = {Invited colloquium talk at Carnegie Mellon University, Math Logic seminar},
institution = {Carnegie Mellon University, Math Logic seminar}