On representing graphs as membership digraphs
Eugenio G. Omodeo, Alexandru I. Tomescu
(Transparencies added in June, scenarios revised in September)
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:
- 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..109, i.e., the whole range of the theorems of our proof scenario on representing 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 representing graphs as membership digraphs takes approximately 15 seconds.
- 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