The idea of this page is to collect questions which might be asked in the exams. Whenever you review the slides or work on exercises, just put anything here which might be asked.

I guess it will be most easy for the moderating group to put questions about the topic they present here, too.

Please try to maintain categories of useful size, so each gets its own edit button.

Please give a short overview over the lecture.

• Intorduction: What is Verification and Specification? What is a Logic? –> Propositional logic

What is Verification?

• argument for building the system right (NOT building the right system –> validation)

What is Specification?

• defining all possible behaviours of the specified syetsm

What is a Model?

What's the most important thing that needs to be proven when defining types in a HOL theory $T = (\chi, \Sigma, A)$?

• Proof that the newly introduced term $S$ of type $r \Rightarrow bool$ has at least one element inside. Formally $T \vdash \exists x.\; S\; x$

Why is it important that the new types defined in HOL are non-empty?

• (see FAQ for hints)

How are the elements True and False introduced in HOL?

• Since there should always be an infinite set in U whose elements and power sets are also fully contained in U, there's a guarantee that there will be a set with two elements and that set is going to represent the values True and False ¹⁾

Why do we need calculi.

Please explain the following properties: Soundness (Correctness), Completeness, …

What are the advantages/disadvantages of the Hilbert calculus compared to the Gentzen calculus.