4 Proof-development in type systems
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.
4.1 Tactics
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 ...
Get Handbook of Automated Reasoning now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
