The representation of Boolean algebras in the spotlight of a proof checker
Rodica Ceterchi, Eugenio G. Omodeo, Alexandru I. Tomescu
June 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 (up to the point where the topological issues enter into play).
- 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..204, i.e., the whole range of the theorems of our proof scenario on representing boolean 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 the representation of Boolean algebras takes about 25 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
