Logik

Winter Semester 2017

Armin Biere, Wolfgang Schreiner, Martina Seidl, Wolfgang Windsteiger

News

• Lecture room moved to HS 2
• Lecture and exercises will start on October 3th, 2017

Schedule

• Lecture: Tuesday, 8:30 - 10:00, HS 2
• Exercises: Tuesday, 10:15 - 11:45, HS 2

Overview

• This course is a first year's Bachelor course.
• For further information on this course, please visit the KUSSS page for the lecture (VL) and the KUSSS page for the exercises.
• Course organization. There will be changes compared to the organization of the last years. Details will be explained in the first lecture.
• Glossary English/German

Slides

We will upate the slides during the semester and they are not considered to be complete until the end of the semester.

• Module: Propositional Logic (SAT)
  • The Decision Problem of Propositional Logic
  • More on Propositional Logic
  • Normal Form Transformation
  • Propositional Reasoning
• Module: First Order Predicate Logic (FO)
  • Syntax and Informal Semantics
  • Reasoning in Predicate Logic
  • Formal Definitions and Specifications
  • Formal Reasoning in Special Domains
  • Formal Semantics and Related Notions
• Module: Satisfiability Modulo Theory (SMT)
  • Satisfiability Modulo Theories (SMT) Basics
  • Satisfiability Modulo Theories (SMT) Details

Exercises

The exercises will be organized via the JKU Moodle.

Resources

Propositional Logic (SAT)

• Limboole

First Order Predicate Logic (FO)

• Theorema
• RISC ProofNavigator
• Thinking Programs

Satisfiabily Modulo Theory (SMT)

• Boolector
• Z3, http://rise4fun.com/z3