Saturday, July 30, 2016

How to verify computer generated proofs that are too long for a human to read?

I propose that a proper implementation of Narwhal could solve this problem. In the previous post I showed how an "if...then" statement could be translated into a proto semantic expression. This would give Narwhal an opportunity to process an arbitrarily long statements and, in particular might be setup to read the proof automatically to determine its correctness. As it crunched along automatically through what would take a lifetime for a human: if an incoherent statement occurs in the proof, or if it finishes and says the proof is true or false, then the final verification would be to verify Narhwal itself.
Verifying Narwhal might be considerably more in the scope of a lifetime. I am sure you could do it by verifying the lowest levels and the inductive/recursive mechanisms for increasing complexity.

No comments:

Post a Comment