AEtnaNova
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
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
Sorted by year (- Avron, Arnon; Cohen, Liron: Applicable mathematics in a minimal computational theory of sets (2018)
- Cantone, Domenico; Longo, Cristiano: A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions (2014)
- Cantone, Domenico; Ursino, Pietro: Formative processes with applications to the decision problem in set theory. II. Powerset and singleton operators, finiteness predicate (2014)
- Milanič, Martin; Rizzi, Romeo; Tomescu, Alexandru I.: Set graphs. II. Complexity of set graph recognition and similar problems (2014)
- Milanič, Martin; Tomescu, Alexandru I.: Set graphs. IV. Further connections with claw-freeness (2014)
- Omodeo, Eugenio G.; Tomescu, Alexandru I.: Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets (2014)
- Milanič, Martin; Tomescu, Alexandru I.: Set graphs. I. Hereditarily finite sets and extensional acyclic orientations (2013)
- Schwartz, Jacob T.; Cantone, Domenico; Omodeo, Eugenio G.: Computational logic and set theory. Applying formalized logic to analysis. Foreword by Martin Davis (2011)