A Computerized Referee

Go Back to Talks and Events

All are welcome to attend the first talk in Seminar in Languages this semester by Prof Eugenio Omodeo. Time: Wednesday 2/4, 3:40pm, Place: Rm.1310

Prof Eugenio Omodeo from University of Trieste in Italy will be visiting us on Wednesday and giving the first talk in Seminar in Languages this semester. Prof Omodeo's main research interests are in automated theorem-proving, logic programming, and set theory.

http://www2.units.it/~eomodeo/publications.html

The Referee system (aka AEtnaNova), accessible on the Web, ingests bodies of text which it either certifies as constituting a valid sequence of definitions and theorems, or rejects as defective.

The functionality of this proof verifier and the key issues for its effective use are illustrated, in particular by case-studies referring to automata and to Stone's representation theorem for Boolean algebras, and through excerpts from a large-scale script which leads from the built-in rudiments of set theory to the formal foundations of mathematical analysis. (The latter scenario, although incomplete as yet, already comprises over 1000 verified proofs, definitions, and 'theories'.) The possibility of exploiting Referee also for algorithm correctness verification is discussed.