New answers tagged software-verification
3
In case you are not aware, there is a possibility that a theorem prover is implemented 100% correctly and run on a faultless machine and proves itself arithmetically inconsistent, even though it is not. The other existing answers focus on the issue of verifying that the theorem prover runs exactly as it was designed to run, but do not address this aspect of "...
5
While this may trend close to self-advertisement, this is essentially the topic of my recent paper Metamath Zero: The Cartesian Theorem Prover (video), and the analogy with bootstrapping compilers is spot on. The introduction of the paper lays out what is needed to make this happen, and it's only a problem of engineering.
As Andrej says, there are several ...
0
This depends on the underlying axioms of the theorem prover. If a prover is based on primitive set theory, it will have few axioms. It can also have optional axioms such as the axiom of choice, which may or may not be useful for higher level proofs. From these primitive axioms and theorems such as Peano arithmetic, we can build up the familiar algebra of ...
40
I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code.
There are many levels of formal verification (that's the phrase you're looking for in place of "proven") of a proof assistant:
Verify that the algorithms used by the proof assistant are correct.
Verify ...
9
What you need is the idea of "the trusted core". Quoting "A verified runtime for a verified theorem prover":
In many theorem provers, the trusted core—the code that must be right to ensure faithfulness—is quite small. As examples, HOL Light is an LCF-style system whose trusted core is 400 lines of Objective Caml, and Milawa is a Boyer-Moore style prover ...
Top 50 recent answers are included
