(Transparencies added in June, scenarios revised in September)

- 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.
- Demo launcher (see instructions for use below).
- Paper illustrating the above scenario.
- Transparencies illustrating the above paper.
- An earlier proof-checking experiment, regarding applications of the graph-representation theorem treated in this page.
- A subsequent proof-checking experiment, about Stone's celebrated representation theorem for Boolean algebras.

The proof-checker AEtnaNova/Referee runs on a server at the University of Trieste and can be accessed through this demo 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)

- 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

- If the list is empty, then all proofs have successfully passed the verification.
- 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**