2
$\begingroup$

More specifically, has anyone used a chain of theorem provers to validate a highly evolved theorem prover, starting with a very simple hand checked prover such that each new theorem prover is used to validate a somewhat more complex theorem prover, rinse repeat?

This would be something along the lines of induction, I guess. In that you'd have just as much confidence in the complex prover at the end as the hand checked prover you started with.

If it has been explored (wouldn't be surprised), a pointer towards more resources would be welcome.

$\endgroup$
2
$\begingroup$

Not that I know of. A more typical architecture is to decompose the theorem prover into a prover plus a proof checker. Then only the proof checker needs to be validated. If proofs are expressed in a simple enough language, then the proof checker might be extremely simple. All of the smarts can go into the prover (which tries various strategies to try to find a valid proof), but it doesn't need to be validated, since its output will always be checked by the proof checker.

$\endgroup$
  • $\begingroup$ Ah, that makes sense. Thanks :-) IIRC from my symbolic logic course, proof checkers are fairly mechanistic and straightforward. Just as a follow up, are there any cases where a proof checker might get complicated? $\endgroup$ – Tyler Spaeth Jul 3 '18 at 11:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.