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.

If there are any answers on this page, they are given by students; Feel free to discuss the answers and/or add additional ones!

Please give a short overview over the lecture.

• Intorduction: What is Verification and Specification? What is a Logic? –> Propositional logic
• Functional programming and specification (ML & Isabelle/HOL)
• HOL: language and semantic aspects (e.g. types, terms, theory, cons. ext., …)
• Proofs in HOL
• Specific things in HOL: sets, functions, relations, and fixpoints
• Verifying functions
• Inductively defined sets
• Specifiaction of PL semantics (operational-, denotational- & axiomatical semantics)
• –> programm verification and programm logic (Hoare 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.

How can we prove formulas without a calculus? * Calculi are based purely on syntax. We can always rely on semantic proofs, e.g. truth table or tableaux methods.