Checking Proofs

Checking proofs

If it cannot be checked, then it is not a proof! If it doesn't generate proofs, then it's not a prover! Bliksem only partially obeys this principle, since it has no way of checking the clause form transformation. However the resolution derivations themselves can be converted into type theory and checked. The programs for doing this are all written in Eclipse Prolog, but there should be no problems running them with other Prolog dialects. The dialect dependent constructions (for filehandling only) are marked by the dialect(X)-predicate.

TT A proof checker, based on type theory. In order to run it you need also the following formalization of intuitionistic first order logic: fol . For the conversion of resolution proofs, only the equality definitions are used.
translate translates proofs by Bliksem into TT-format. In order to be able to convert the proof, one needs to set the following options in the input file to Bliksem.
```
Set( prologoutput, 2 ).
Set( totalproof, 1 ).
   
```
If a proof is found, then the part between the strings
```
% ABCDEFGHIJKLMNOPQRSTUVWXYZ
   
```
should be read by translate.pro . There is currently no tool to extract the relevant part from the proof, this has to be done by hand in an editor. Inside Eclipse, type
```
      ['translate.pro']. 
      translate( 'File1', 'File2' ).
   
```
File1 is the name of the output of Bliksem. File2 is the file in which the translation will be written.
There is a little technical problem. The outpufile of translate.pro contains lines which are far too long. Use the program linecut.c to cut long lines. linecut.c does this in a civilized manner, in particular not in the middle of an identifier. At the shell, type
```
linecut < File2 > File3
   
```
The result can be checked by TT. Inside Eclipse, type
```
['tt.pro'].
include( 'File3' ).
   
```
coq.pro . Translates from TT-format into Coq format. Inside Eclipse, type
```
['coq.pro'].
translate( 'File3', 'File4' ).
   
```
The output has to be cut again by linecut.c , resulting in File5. File5 can be entered into Coq by cut-and-paste, or by typing
```
Load File5.
   
```
inside Coq.

The theoretical foundations for translate.pro are based on joint work with Marc Bezem and Dimitri Hendriks .

Checking proofs

Other links: