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 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) |