Computational Logic
Department of Computer Science - Universität Innsbruck
  • Home
  • Research
    • Publications
    • Projects
    • Software
  • Teaching
  • Members
    • Aart Middeldorp
      • Edited Books
  • Events
    • Event Archive
  • News
    • News Archive
  1. You are here:  
  2. Home
  3. Teaching
  4. SS 2025

Logic


Lecturers: Aart Middeldorp, Alexander Montag, Johannes Niederhauser, Daniel Ranalter, Vera Schmitt, Sven Goetzke, Harald Zankl


News: Check this site regularly for announcements; visit the content to access the slides, the homework exercises, as well as selected solutions.
Registration: Online registration for the exercises (PS) is required until 23:59 on February 21 and for the lecture (VO) until 23:59 on June 30.
Registration: Online registration is required between August 21 and September 11 (23:59) for the 2nd exam on September 25.
Registration: Online registration for the PS is required until 23:59 on February 21. Groups 1 and 6 are taught in English, groups 2, 3, 4 and 5 are taught in German.
Content: The course provides an introduction to logic and model checking.
DateTopicsSlidesExcercisesSolutions
03.03 & 06.03 & 13.03 propositional logic, satisfiability, validity, conjunctive normal forms pdf (x1, x4)  pdf  pdf
10.03 & 20.03 Horn formulas, SAT, Tseitin's transformation pdf (x1, x4)  pdf  pdf
17.03 & 27.03 natural deduction, soundness pdf (x1, x4)  pdf  pdf
24.03 & 03.04 completeness, resolution, binary decision diagrams  pdf (x1, x4)  pdf  pdf
31.03 & 10.04 binary decision diagrams, predicate logic (syntax) pdf (x1, x4)  pdf  pdf
07.04 & 08.05 predicate logic (semantics), natural deduction pdf (x1, x4)  pdf  pdf
28.04 & 08.05 quantifier equivalences, unification, Skolemization  pdf (x1, x4)  pdf  pdf
05.05 & 15.05 resolution, undecidability, algebraic normal forms  pdf (x1, x4)  pdf  pdf
12.05 & 22.05 Post's adequacy theorem, CTL, CTL model-checking algorithm pdf (x1, x4)  pdf  pdf
19.05 & 05.06 symbolic model checking, LTL pdf (x1, x4)  pdf  pdf
26.05 & 12.06 adequacy, fairness, LTL model-checking algorithm pdf (x1, x4)  pdf  pdf
02.06 & 12.06 CTL*, SAT solving, sorting networks pdf (x1, x4)   pdf  pdf
16.06 SAT solving, sorting networks pdf (x1, x4)   pdf  pdf
23.06 1st exam (solution)      
25.09 2nd exam      
26.02 3rd exam      

Literature

The course is largely based on the following book:

  • Michael Huth and Mark Ryan
    Logic in Computer Science (second edition)
    Cambridge University Press, 2007
    ISBN 0-521-54310-X (paperback)

Slides as well as solutions to selected exercises will be made available online.

Subcategories

Page 3 of 3

  • 1
  • 2
  • 3

© 2025 Computational Logic

g48
  • Contact
  • Data and Privacy
  • Something
  • FAQs
  • About