Inhalt
- Was ist ein Beweis?
- Wann ist ein Beweis detailiert genug?
- Im Beweisassistent ROCQ sind Beweise Programme!
- Aussagen = Typen
- Beweise = Programme
- Beweis-Checker = Compiler
- Damit lassen sich in ROCQ nicht nur Programme schreiben, sondern man kann direkt noch deren Korrektheit zeigen.