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.
- Scenario of the proofs, in the keyboard-oriented format in which it gets submitted to Ref. (Explanations are included in the form of comments.)
- Pretty-printed scenario of the same proofs. (Version devoid of comments.)
- Demo launcher (see instructions for use below).
- Paper illustrating the above scenario. (Original version: This paper underwent substantial revision.)
- Paper in the final form in which it was published
- Another paper, comprising the above pretty-printed scenario as an appendix, with explanations added in the form of comments.
- A subsequent proof-checking experiment, regarding the graph-representation theorem per se.
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:
- Me: the username running the verification; the default value is Gue, a Guest account created for the present purpose
- Verify: the range of theorems to be checked; the default value of this launcher is 1..50, i.e., the whole range of the theorems of our proof scenario on claw-free graphs
- More Files: the user can load up to three different proof scenarions, as plain text files.
- For the present purpose, a user must first download locally the text of the proof scenario, which must then be uploaded in the first file field of More Files
- The verification starts once the user presses GO
- The verification of the entire proof scenario on claw-free graphs takes about 3 minutes.
- For a quicker hands-on experimentation with the verifier, one can just restrict the range of the theorems to be checked, e.g. 1..10
- Setting the Verify range to 1 will force Referee, besides verifying the first submitted theorem, to activate a display mode of all the theorems, definitions and THEORYs, together with a citation map, of the submitted proof scenario (see the picture at the bottom of the page)
How to read the output:
- The default view of the output page lists the theorems whose proofs Referee considers to be erroneous.
- If the list is empty, then all proofs have successfully passed the verification.
- Otherwise, Referee will indicate the problematic inference setps, as shown below
- For the list of correct proofs, the user must click on the radiobox Good Pfs. at the top of the page
- The list of all theorems, definitions and THEORYs, together with a citation map, of the submitted proof scenario is displayed if the Verify range is set to 1