Logik

Winter Semester 2018

Armin Biere, Wolfgang Schreiner, Martina Seidl, Wolfgang Windsteiger

News

• Lecture and exercises will start on October 2nd, 2018

Schedule

• Lecture: Tuesday, 8:00 - 9:30, HS 16
• Mini Test: Tuesday, 9:40 - 9:55, HS 16
• Exercises: Tuesday, 11:00 - 11:45, HS 18

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 (version of 2018). There are 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)
• SAT Basics I (Changes in Version 2018.2: added slides 31-33 (resolution))
• SAT Basics II (Changes in Version 2018.2: added slides 30 - 41)
• SAT Reasoning
• Module: First Order Predicate Logic (FO)
• Syntax
• Semantics
• Pragmatics
• Formal Reasoning
• Special Topics
• 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)

• RISCAL (README, VirtualBox Video, X2Go Video)
  • Demo Video (pdf, txt)
  • The visualization feature of RISCAL is currently disabled in the X2Go installation (only enabled in the VirtualBox machine).
• Theorema
• Thinking Programs

Satisfiabily Modulo Theory (SMT)

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