TU Wien:Logic and Computability VU (Ciabattoni)/Oral Exams

Aus VoWi
Zur Navigation springen Zur Suche springen

2020-01[Bearbeiten | Quelltext bearbeiten]

Part 1:

  • Proof of Rice's Theorem.
  • Sketch of the proof of completeness for FOL, meaning more or less describe the different cases and what is the idea in each case (we didn't really go deep into the details, although she asked what was the general idea of the search algorithm used in that proof)

Part 2:

  • Theorem GT, difference with Gödel incompleteness
  • Why are there so many modal logics, examples, meaning of box in these examples.
  • Meaning of different connectors in BHK semantics

2020-06[Bearbeiten | Quelltext bearbeiten]

Corona Mode (written and oral part combined the oral online exam)

Part 1:

  • Proof
  • Proof
  • Is recursive, r.e. or none? How about without the second conjunct?
  • Is recursive, r.e. or none?
  • Correctness proof of sequent calculus for prop. logic. How does the proof differ when extending the calculus to PL1? (no details about the PL1 proof required)
  • Proof of Post theorem

Part 2:

  • Is there a MGU for If yes, what is an MGU, if no why not?
  • Does the formula "Diamond A implies Box A" characterize linearity (i.e. each world has at most one successor)? If yes, give a proof idea, if no give a counterexample.
  • Give a proof for
  • Meaning of different connectors in BHK semantics
  • Theorem GT, difference with Gödel incompleteness
  • Why is Gödel's incompletenes theorem important for software verification?

2020-09[Bearbeiten | Quelltext bearbeiten]

(still Corona Mode)

Part 1:

  • Proof using LK
  • Proof using LK
  • Is recursive, r.e. or none?
  • Post Theorem (what does it say + proof)
  • Completeness of LK for FOL (idea of proof search algorithm, case distinctions - very general)

Part 2:

  • If possible, compute mgu of (separately) and of (a and u are constants). If not, why not?
  • Show frame for which does not hold; prove that it characterizes linearity
  • Show that is valid in IL using BHK semantics (what about if you have instead?). Explain why is not valid in IL.
  • What is refutational completeness? What is its significance for automated deduction?
  • Difference GT and GI (high-level)
  • Generally questions during the exercise part (I don't remember them exactly)