×

AEtnaNova

swMATH ID: 6360
Software Authors: Omodeo, Eugenio G.; Cantone, Domenico; Policriti, Alberto; Schwartz, Jacob T.
Description: 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
Homepage: http://link.springer.com/chapter/10.1007/11829263_7
Related Software: Referee; SETL; Mizar; Metamath; Nuprl; Isabelle/HOL; Archive Formal Proofs; Dijkstra Shortest Path; Isar; ACL2; Datalog
Cited in: 9 Documents
all top 5

Cited by 11 Authors

4 Cantone, Domenico
4 Tomescu, Alexandru Ioan
3 Milanič, Martin
2 Omodeo, Eugenio Giovanni
2 Ursino, Pietro
1 Avron, Arnon
1 Cohen, Liron
1 Davis, Martin David
1 Longo, Cristiano
1 Rizzi, Romeo
1 Schwartz, Jacob Theodore
all top 5

Cited in 6 Serials

2 Discrete Applied Mathematics
2 Theoretical Computer Science
1 Information and Computation
1 Journal of Automated Reasoning
1 ACM Transactions on Computational Logic
1 Logical Methods in Computer Science

Cited in 4 Fields

6 Mathematical logic and foundations (03-XX)
4 Combinatorics (05-XX)
4 Computer science (68-XX)
1 Functions of a complex variable (30-XX)

Citations by Year