[FOM] mechanical theorem metachecking
Martin Davis
martin at eipye.com
Wed Oct 8 00:24:11 EDT 2008
On October 6 Hendrik wrote:
>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?
This question is discussed and a suitable meta-theorem proved in the paper:
Martin Davis & J.T. Schwartz, ``Metamathematical Extensibility for Theorem
Verifiers and Proof-Checkers,'' Computers and Mathematics with
Applications, vol.5(1979), pp. 217-230.
Martin
Martin Davis
Visiting Scholar UC Berkeley
Professor Emeritus, NYU
martin at eipye.com
(Add 1 and get 0)
http://www.eipye.com
More information about the FOM
mailing list