Collecting proofs of the same theorem in various proof checking systems
may be useful for preparing a thorough comparative survey of existing
systems( I would be grateful for any references on such surveys already
published).
Maybe such a survey could clarify that different systems in some cases
use actually similar language constructs (from the point of view of absract
syntax) but expressed in a different concrete syntax.
Another related problem is an explication of the notion "proof".
The usual definition of proof as " a finite sequence of one or more
formulas each of which either is an axiom or is immediatedly inferred
from preceding formulas in the sequence by means of one of the rules
of inference" is unsatisfactory for our goals because:
1) This definition is good for "bottom-up" proofs, but real proofs may
be "top-down", that is, a formula in a top-down proof may be inferred
using also some succeding formulas;
2) A real proof may contain not only formulas but also some definitions;
Maybe for our goals it is better to define a proof as a dag; a formula
and an inference rule are attached to every vertex of the dag;
then various syntaxes for writing proofs could be considered as various
ways of flattenning this dag.
Below is a proof of a well-known theorem checked recently by Veda:
-- external files
{
c:\veda\snam.ved -- it is the file containing definitions
-- of all predefined names(int, +, bool, A, E ...)
}
-- The set of all prime numbers is infinite 02/20/96
[
x:int! y:int! z:int ;
-- for brevity some obvious auxiliary facts are expresed as defining axioms
def[fact; fn(int,int); fact(x) + 1 > x |
y \ (fact(x) + 1) -> y > x];
def[prim; fn(int,bool);
~(prim(x)) -> E[z:int, z \ x & z>1 & z<x & prim(z)]];
def[\; fn([int,int],bool)];
proofr([ -- proof by reductio ad absurdum
A[x:int, E[y:int, prim(x) -> y>x & prim(y)]]; -- the theorem
-- !E[x:int, A[y:int, prim(x) &(~ y>x or ~ prim(y))]]; -- the negation
-- the system builds the negation automaticlly and marks it as true
s2 := def[c; int; A[y:int, prim(c) & (~( y>c) or ~(prim(y)))]];
F := fact(c) + 1;
s3 := F > c; logic(s3,fact); -- from def: fact(x) + 1 > x
s4 := ~(prim(F)); logic(s4,s3,c); -- from s2, s3
s5 := E[z:int, z \ F & z>1 & z<F & prim(z)]; logic(s5,s4,prim);
s6 := def[z; int; z \ F & z>1 & z<F & prim(z)];
s7 := z > c; logic(s7, z, fact); -- from z \ F in def z
-- and y \ (fact(x) + 1) -> y > x in def fact
s8 := prim(z); logic(s8, z); -- from def z
s9 := ~(z > c); logic(s9, s8, c) -- from s2, s8
-- contradiction s7, s9
]) -- end proof
]