On representing graphs as membership digraphs

Eugenio G. Omodeo, Alexandru I. Tomescu

May 2014
(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.

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