[FOM] mechanical theorem metachecking

[Roger Bishop Jones]

On Wednesday 08 October 2008 05:24:11 Martin Davis wrote:

> 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.

And also more recently (1995) in:

Metatheory and Reflection in Theorem Proving:A Survey and Critique

by John Harrison

available online at:

http://www.cl.cam.ac.uk/~jrh13/papers/reflect.html

[and in lots of other places, a google for metatheory and reflection gives 
24000 hits]

Roger Jones