Logic

Winter Semester 2020

Armin Biere, Wolfgang Schreiner, Martina Seidl, Wolfgang Windsteiger

News

• Lecture and exercises will start on October 6th, 2020.
• The whole course will be held online because of Corona.

Schedule

• Lecture: recordings will be provided weekly
• Weekly Mini Test: Tuesday, 10:00 - 10:45 online in Moodle + Zoom (alternative: big exam at the end of the semester)
• Exercises: Tuesday, 10:45 - 11:45, live stream

Overview

• This course is a first year's Bachelor course.
• Please register in KUSSS page for the lecture (VL) and the
  • KUSSS page for the exercises if you are in Linz
  • KUSSS page for the exercises if you are in Vienna
• Glossary English/German

Slides and Lecture Notes

We will update the material during the semester; it is not considered to be complete until the end of the semester.

• Slides on Course Organization
• Module: Propositional Logic (SAT)
• Lecture 1
• Lecture 2
• Lecture 3
• Lecture 4
• Module: First Order Predicate Logic (FO)
• FO: Syntax, Semantics, Pragmatics
  • Syntax
  • Semantics
  • Pragmatics
• FO: Reasoning
  • Formal Reasoning
  • Special Topics
• Module: Satisfiability Modulo Theories (SMT)
• SMT Basics
• SMT Details

Exercises

The exercises will be organized via Moodle

Resources

Propositional Logic (SAT)

• Limboole

First Order Predicate Logic (FO)

• RISCAL (README, VirtualBox Video, X2Go Video)
  • Demo Video (pdf, txt)
• Theorema

Satisfiabily Modulo Theory (SMT)

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