There are many computational theorem provers, such as Z3 (http://z3.codeplex.com/). Such provers employ many thousands of lines of code. How can one prove that the results are correct and can be trusted?

  • $\begingroup$ Even if there was such a proof, Donald Knuth would say: "Beware of bugs in the above code; I have only proved it correct, not tried it." :) $\endgroup$ – PhoemueX Jan 6 '15 at 6:42
  • $\begingroup$ @PhoemueX, indeed. My interest is in autonomous systems, where it is certainly desirable to have provably correct decisions being made by a machine. An analogous approach used for high-reliability engineering employs triple-modular-redundancy (TMR). Three different implementations, then majority voting on the results. I presume one could employ the same approach for this application using three different logic solvers and ensure that their results are equivalent (perhaps yet another challenge). $\endgroup$ – Alan Jan 6 '15 at 11:39

Your Answer

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

Browse other questions tagged or ask your own question.