Computational Logic (WS 2022/23)

Section outline

• Select section General

  General

  Collapse all Expand all

  326.010/326.011, Monday 15:30-17:00 (Lecture), 17:15-18:00 (Exercises), Room: S2 053, Start: October 10, 2022

  This course gives an introduction to computational logic, i.e., to those aspects of logic that can be supported by software and/or are relevant for software development: satisfiability solving in propositional logic, computer-supported and fully automated proving in first-order logic, and decision procedures for certain (combinations of) logical theories. In line with the topic of this course, the theory will be explained with the help of software that implements this theory. Furthermore, we will present computational tools that are actually used in real life and demonstrate their practical application.

  You have to create an account in this Moodle instance and self-register as a course participant (link "Enrol me in this course" at the top). You are then able to submit your assignments; furthermore, you receive per email all messages posted in the "Announcements" forum and may yourself post messages in the "Questions and Answers" forum.
  
• Select section Course Videos

  Course Videos

  As an extra service, we intend to live-stream and record the lectures via the following Zoom session:

  
  

  https://jku.zoom.us/j/95970972547?pwd=VmZic3dzb3VRMldYOHV3SkcydEtCQT09
  Meeting Id: 959 7097 2547 Password: complogic

  
  

  However, no guarantee is given with respect to completeness and quality of the stream/recordings. The basic course format is on-site, not hybrid.
  

  • Select activity Video Lecture October 10, 2022

    

    Video Lecture October 10, 2022 URL
  • Select activity Video Lecture October 17, 2022

    

    Video Lecture October 17, 2022 URL
  • Select activity Video Lecture October 24, 2022

    

    Video Lecture October 24, 2022 URL
  • Select activity Video Lecture October 31, 2022

    

    Video Lecture October 31, 2022 URL
  • Select activity Video Lecture November 7, 2022

    

    Video Lecture November 7, 2022 URL
  • Select activity Video Lecture November 14, 2022

    

    Video Lecture November 14, 2022 URL
  • Select activity Video Lecture November 21, 2022

    

    Video Lecture November 21, 2022 URL
  • Select activity Video Lecture November 28, 2022

    

    Video Lecture November 28, 2022 URL
  • Select activity Video Lecture December 5, 2022

    

    Video Lecture December 5, 2022 URL
  • Select activity Video Lecture December 12, 2022

    

    Video Lecture December 12, 2022 URL
  • Select activity Video Lecture January 9, 2023

    

    Video Lecture January 9, 2023 URL
  • Select activity Video Lecture January 16, 2023

    

    Video Lecture January 16, 2023 URL
  • Select activity Video Lecture January 23, 2023

    

    Video Lecture January 23, 2023 URL
• Select section Lecture

  Lecture

  • Select activity Software Examples

    

    Software Examples File
  • Select activity Computational Logic: Course Introduction and Organization

    

    Computational Logic: Course Introduction and Organization File
  • Select activity Propositional Logic: Syntax and Semantics

    

    Propositional Logic: Syntax and Semantics File
  • Select activity Propositional Logic: Proofs

    

    Propositional Logic: Proofs File
  • Select activity Propositional Logic: Modern SAT Solving

    

    Propositional Logic: Modern SAT Solving File
  • Select activity Propositional Logic: Applications of SAT Solving

    

    Propositional Logic: Applications of SAT Solving File
  • Select activity First-Order Logic: Syntax and Semantics

    

    First-Order Logic: Syntax and Semantics File
  • Select activity First-Order Logic: Proofs

    

    First-Order Logic: Proofs File
  • Select activity First-Order Logic: Software for Proving

    

    First-Order Logic: Software for Proving File
  • Select activity First-Order Logic: The Method of Analytic Tableaux

    

    First-Order Logic: The Method of Analytic Tableaux File
  • Select activity First-Order Logic: The Resolution Method

    

    First-Order Logic: The Resolution Method File
  • Select activity First-Order Logic: Reasoning About Equality

    

    First-Order Logic: Reasoning About Equality File
  • Select activity SMT Solving: Decidable Theories

    

    SMT Solving: Decidable Theories File
  • Select activity SMT Solving: Combining Decision Procedures

    

    SMT Solving: Combining Decision Procedures File
• Select section Exercises

  Exercises

  Each exercise sheet allows you to earn 100 grade points. The best 8 sheets will be used for calculating the grade: >= 400 GEN4, >= 500 BEF3, >= 600 GUT2, >= 700 SGT1.
  

  • Select activity Assignment 1 (October 30)

    

    Assignment 1 (October 30)

    Due: Sunday, 30 October 2022, 11:59 PM
  • Select activity Assignment 2 (November 6)

    

    Assignment 2 (November 6)

    Due: Sunday, 6 November 2022, 11:59 PM
  • Select activity Assignment 3 (November 13)

    

    Assignment 3 (November 13)

    Due: Sunday, 13 November 2022, 11:59 PM
  • Select activity Assignment 4 (November 20)

    

    Assignment 4 (November 20)

    Due: Sunday, 20 November 2022, 11:59 PM
  • Select activity Assignment 5 (November 27)

    

    Assignment 5 (November 27)

    Due: Sunday, 27 November 2022, 11:59 PM
  • Select activity Assignment 6 (December 4)

    

    Assignment 6 (December 4)

    Due: Sunday, 4 December 2022, 11:59 PM
  • Select activity Assignment 7 (December 11)

    

    Assignment 7 (December 11)

    Due: Sunday, 11 December 2022, 11:59 PM
  • Select activity Assignment 8 (January 8)

    

    Assignment 8 (January 8)

    Due: Sunday, 8 January 2023, 11:59 PM
  • Select activity Assignment 9 (January 15)

    

    Assignment 9 (January 15)

    Due: Sunday, 15 January 2023, 11:59 PM
  • Select activity Assignment 10 (January 22)

    

    Assignment 10 (January 22)

    Due: Sunday, 22 January 2023, 11:59 PM
• Select section Software

  Software

  The following software is used/demonstrated in this course (this software is all pre-installed on a virtual machine for your easy use):

  • Code and resources for “Handbook of Practical Logic and Automated Reasoning”
    
  • Sequent Calculus Trainer
    
  • The MiniSat Page
    
  • Limboole
    
  • The RISC Algorithm Language (RISCAL)
    
  • The RISC ProofNavigator
    
  • Tree Proof Generator
    
  • SWI Prolog
    
  • Vampire
    
  • Isabelle
    
  • The Z3 Theorem Prover
    
• Select section Lecture Exam

  Lecture Exam

  • 2nd Exam: Wednesday, March 29, 2023, 17:15-18:45, S3 047
    
    • Registration in KUSSS is required till Monday, March 27, 12:00.
      
    • Open book (all printed/written materials allowed).
      
    • The questions will be similar to those from the exercise sheets.

  • Select activity Sample Exam Questions

    

    Sample Exam Questions File
  • Select activity Lecture Exam (January 30, 2023)

    

    Lecture Exam (January 30, 2023) Assignment

    Due: Monday, 30 January 2023, 5:15 PM