FOM: 107:Automated Proof Checking

[Freek Wiedijk]

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:

	<http://www.cs.kun.nl/~freek/notes/by.ps.gz>

>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