The representation of Boolean algebras in the spotlight of a proof checker

Rodica Ceterchi, Eugenio G. Omodeo, Alexandru I. Tomescu

June 2014

The main publication about the proof-checker used to develop these formal proofs is this monograph.
The proof-checker AEtnaNova/Referee runs on a server at the University of Trieste and can be accessed through this demo launcher.

For a basic use of the system, one has to fill in the following fields of the launcher:

How to read the output: