In this section we will show how a concrete proof-assistant works. First we show in what way the human has to interact with the system. Then a small proof-development is partially shown (most proof-objects are omitted). Finally it is shown how computations can be captured in formalized theories.

In Section 2.1 and Section 4.3 examples will be given of an easy, and a more involved theorem with full proofs. Even before these examples are given, the reader will probably realize that constructing fully formalized proofs (the proof-objects) is relatively involved. Therefore tools have been developed—so-called proof-assistants— that make this task more easy. A proof assistant consists of a proof ...

Start Free Trial

No credit card required