Logik

Winter Semester 2016

Armin Biere, Wolfgang Schreiner, Martina Seidl, Wolfgang Windsteiger

News

• Lecture and exercises will start on October 4th, 2016

Schedule

• Lecture: Tuesday, 8:30 - 10:00, HS 18
• Exercises: Tuesday, 10:15 - 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
• 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)
  • Introduction
  • Basic Propositional Logic
  • Propositional Logic Checking
• 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