FOM: 107:Automated Proof Checking

Freek Wiedijk freek at
Sat May 26 14:06:15 EDT 2001

Dear Harvey Friedman,

>We use the key concept of SELF PROVING SEQUENT.

The Mizar system has a very similar concept, although it's
not called like that.  It is the basic inference step of
Mizar.  Andrzej Trybulec described its implementation to me
by e-mail.  His explanation is on the web at:


>Every claim is labeled as such, and is in the following form:
>	Assume A1,...,Ak. Then B.

This looks very similar to the Mizar statement:

	B by A1,...,Ak;

Freek Wiedijk

More information about the FOM mailing list