Reasoning about connectivity without paths

Alberto Casagrande, Eugenio G. Omodeo

September 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: