Claw-free graphs as sets -- Proofs of existence of a near-perfect matching and of Hamiltonicity in their square.

Eugenio G. Omodeo, Alexandru I. Tomescu

November 2011 (revised in August 2012 and in 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: