[FOM] mechanical theorem metachecking
hendrik@topoi.pooq.com
hendrik at topoi.pooq.com
Mon Oct 6 23:06:03 EDT 2008
I've been wondering about the possibility of mechanical theorem
metachecking.
Let's say we have a formal system F.
In F, we prove that the execution of some computer program P(x) will,
if it terminates, always generate a formula that is provable in F.
Since execution of P on a machine may be more efficient than
checking the proof it generates, we're tempted to include a rule
that allows us to use such proved programs as proof rules in F.
Under what circumstances is it possible to do this safely?
If it is impossible as stated, what variations on the question could
yield safe proof-checking?
-- hendrik
More information about the FOM
mailing list