Instructors

Grading policy

Exam Results

The results of the reexamination are available here. You may see your paper on Thursday starting at 14h by appointment at stefan.ciobaca@gmail.com.

How to Study

Syllabus (tentative)

Week 1 - Introduction to Informal Logic

Lecture notes: PDF.

Exercises for tutorial: PDF.

Week 2 - The Syntax of Propositional Logic

Lecture notes: PDF.

Exercises for tutorial: PDF.

Support application 1 - determines whether a string is a PL formula.

Support application 2 - determines and explains the subformulae of a PL formula.

Support application 3 - computes the abstract syntax tree (ast) of a PL formula.

Support application 4 - computes (and explains) the height of (the ast of) a PL formula.

Support application 5 - computes (and explains) the size of (the ast of) a PL formula.

Support application 6 - computes (and explains) the set of propositional variables occuring in a PL formula.

Support application 7 - computes the abstract syntax tree of a PL formula without all brackets based on the priority of the logical connectives.

Week 3 - The Semantics of Propositional Logic

Lecture notes: PDF.

Exercises for tutorial: PDF.

Week 4 - The Satisfiability Problem

Lecture notes: PDF.

Exercises for tutorial: PDF.

Backtracking search for CNF-SAT: back.c.

Example files for CNF-SAT: examples folder.

Benchmark files for showcasing exponential running time of back.c: benchmark folder.

Tutorial homework (SUDOKU solver, fill in the missing code) sudoku folder.

The SAT Competition: satcompetition.org.

The MiniSAT Solver: http://minisat.se/MiniSat.html.

An online sat solver: https://jgalenson.github.io/research.js/demos/minisat.html.

Week 5 - Natural Deduction

Lecture notes: PDF.

Exercises for tutorial: PDF.

Support application 1: link.

Week 6 - Advanced Topics in Propositional Logic (This Year: Propositional Resolution)

Lecture notes: PDF.

Exercises for tutorial: PDF.

Week 7 - Functions, Predicates and Structures

Week 8 - Syntax of first-order logic

Lecture notes: PDF.

Exercises for tutorial: PDF.

Try Z3 online here (or download it from here).

Download SPASS from here.

Examples for Z3 and SPASS: here.

Week 9 - Semantics of First-Order Logic

Lecture notes: PDF.

Exercises for tutorial: PDF.

Week 10 - Normal Forms 1

Lecture notes: PDF.

Exercises for tutorial: PDF.

Part of the next tutorial is dedicated to experimenting with the Z3 prover, developed by Microsoft. There are two ways of running Z3. The first is to use the online interface at: https://rise4fun.com/z3. For this version, it is sufficient to write the code in the textbox and push the Play button. The second possibility is to download the version of Z3 specific to your system from the following URL: https://github.com/Z3Prover/z3/releases. In this case, you must save the code to a text file and run Z3 using the command line "path\to\z3.exe filename.txt". I recommend that you preinstall Z3 to avoid connectivity issues.

Week 11 - Normal Forms 2, Ground Resolution

Lecture notes: PDF (RO).

Exercises for tutorial: PDF.

English lecture notes will be available soon.

If there are any mistakes in the grading file, please let me know until the end of the year.

Week 12 - Unification and Resolution

Lecture notes: PDF (RO).

Exercises for tutorial: PDF.

English lecture notes will be available soon.

Week 13 - First-Order Logic with Equality; First-Order Theories.