CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishThe 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 a case-study referring to bisimulations, 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 paper also discusses enhancements to Referee which are in progress: a new inference mechanism, named proof-by-structure, whose addition should make proofs lighter and more readable; an interface to external provers; and an automatic proof optimizer (currently being tested), aimed at speeding up proof verification.
| Titolo: | A Computerized Referee |
| Autori interni: | |
| Data di pubblicazione: | 2006 |
| Rivista: | |
| Handle: | http://hdl.handle.net/20.500.11769/60614 |
| Appare nelle tipologie: | 2.1 Contributo in volume (Capitolo o Saggio) |
File in questo prodotto:
http://hdl.handle.net/20.500.11769/60614
Copyright © 2021