[Talks@IDSIA] 11.06 1430 IDSIA - Marco Caminati. Computer-aided mathematical proofs

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.