Monday 11 June 2012, 1430
IDSIA meeting room, Galleria 1, Manno
SPEAKER:
Marco Caminati, University of Rome "La Sapienza", Italy
TITLE:
Computer-aided mathematical proofs
ABSTRACT:
Theorem provers are computer programs aiming to find, help to find, or merely certify
mathematical proofs, given a formal language and a set of inference rules.
After an introduction about the current state of the field, I will focus on proofs in the
standard mathematical formal language (set theory) and on Mizar, arguably the most
developed software project in this framework.
More precisely, I will give a review of the issues involved in formalizing fundamental
results (like Goedel's completeness and Lowenheim-Skolem theorems) concerning
first-order logic into (set theory + inference rules), which is a first-order logic
itself.
Show replies by date