After successful completion of the course, students are able to

• define syntax and semantics of propositional logic and quantified Boolean formulas,
• develop proofs in calculi for the mentioned logics,
• argue soundness and completeness of the proof pocedures (including extensions),
• use the solvers in practise.

• Syntax, semantic, etc. for the mentioned logics proof
• Procedures for these logics especially for quantified Boolean formulas
• New developments like, e.g., solver in non-normal form, circuits, certificates and their extraction from proofs etc.
• Practical work with selected provers and implementations (e.g., preprocessors).
• A more detailed presentation of the content of the summer term will be presented in the first lecture

• Traditional lecture format supported by lecture videos
• Supporting Q+A sessions
• Practical work with solver

ECTS breakdown

• 18h: 9 lectures a 2h
• 15h: 3 ex sheets a 5 ex; including preparation of a solution in pdf)
•  6h: ex presentation
•  8h: reading a research paper (in teams of 2 students)
• 12h: preparation of paper presentation
•   7h: presentation (10 teams, 3 presentations in a 2h slot)
•   8h:preparation for final exam
•  1h: final exam

 Attention: The dates for the exams are from last year. They will be discussed in the first lecture "Vorbesprechung"

Choise between presentation, or implementation of an additionsl proof technique plus an oral exam

Current literature like journal articles, articles from the Handbook of Satisfiability, etc. will be discussed during the lecture.

1) Propositional and predicate logic

   a) Syntax, normal forms and normal form translations

   b) Semantics, evaluation of a given formula with respect to a given interpretation, the concept of logical    consequence (entailment) also under theories, Translation of  validity, entailment, equivalence and satisfiablity problems into each other, proof procedures (beeing able to apply tableau, sequent  systems or NK)

2) Ability to construct simple proofs

   a) Induction proofs (for simple examples

   b) Simple proofs of run-time or space estimations (Example: Show that the time complexity of breadth first search with a fixed branching degree b and depth d is in O(b^d). I expect a formally correct proof  including explanations (e.g., for the O-notation).

The previous knowledeg had been taught in the course "Theoretischer Informatik und
Logik" (TIL),  "formalen Methoden der Informatik" (FMINF), "Algorithmen und Datenstrukturen" and
math lectures from the beginning of our bachelor studies.  For a part of the knowledge about logic,
  the slides of TIL and from the block Satisfiability (SAT) of FMINF  (http://www.logic.at/lvas/fminf/) could be helpfull.