## Reasoning about connectivity without paths

### Alberto Casagrande, Eugenio G. Omodeo

#### September 2014

####
- 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.

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..46**, i.e., the whole range of the theorems of our proof scenario on reasoning about hypergraph connectivity without paths
**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 hypergraph connectivity takes less than 5 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**