Course with SWS 2/2/0 (lecture/exercise/practical) in WS 2015
- Written exam
This course will introduce you to propositional logic and first-order predicate logic. After reviewing syntax and semantics, we will cover some basic concepts like normal forms, substitution, and unification. You will be introduced to proof procedures such as the resolution calculus and related concepts including soundness, completeness, and decidability.
The lecture ends on November 25, and we continue with Science of Computational Logic
Please pay attention to our guidelines.
We plan to run two test exam where participation is compulsory and results will count for 10% of the final grade.
Test Exam 1: Monday 2th November
Test Exam 2: Wednesday, 9th December
Final Exam: 19th December, 10am in Room ZEU/255/Z (Zeunerbau, Georg-Bährstrasse 3c).
This course will be examined as a part of the Foundations exam. The Foundation exam consists of two separate exams: a written examination for the course Logic and an oral examination for the course Science of Computational Logic. The written exam is scheduled shortly before Christmas.
Some remarks on the style of the written exam in logic
- no exam aids or support materials will be allowed. In other words, only writing materials are allowed.
- The emphasis of the exam will be on the proofs of theorems, propositions and lemmata from the lectures and the proofs occurring with the problems from the tutorials.
- In addition, in the first problem of the exam we will usually ask for some definition or algorithm presented on the lectures, e.g. define concepts like substitution, resolvent, interpretation, Skolemization, ... or algorithms like unification, transformation to clause form, ...
- Maybe, one or two exam problems will be the application of some of the presented calculi (e.g. resolution, natural deduction, normalform transformation, etc).
|Lecture||Lecture - History of Logic and Propositional Logic, till slide 'recursion'||DS6, October 12, 2015 in APB E005||File 1, File 2|
|Lecture||Lecture - Propositional Logic, till 'Replacement Theorem' (slide 27)||DS2, October 14, 2015 in APB E005|
|Exercise||Tutorial: Training on Induction, Recursive Functions||DS4, October 15, 2015 in APB E005||File|
|Exercise||Tutorial: The set L(R)||DS5, October 16, 2015 in APB E005|
|Lecture||Lecture||DS6, October 19, 2015 in APB E005|
|Lecture||Lecture, till slide 62||DS2, October 21, 2015 in APB E005|
|Exercise||Tutorial: Training on entailment, proof structure (iff, implication), counter examples||DS4, October 22, 2015 in APB E005|
|Exercise||Tutorial: Entailment and unsatisfiability, proof structure||DS5, October 23, 2015 in APB E005|
|Lecture||Lecture||DS6, October 26, 2015 in APB E005|
|Lecture||Lecture - finished propositional logic||DS2, October 28, 2015 in APB E005|
|Exercise||Tutorial: Replacement Theorem and Normal Forms||DS4, October 29, 2015 in APB E005|
|Exercise||Tutorial: Resolution||DS5, October 30, 2015 in APB E005|
|Lecture||Test Exam I||DS6, November 2, 2015 in APB E005|
|Lecture||Introduction into Predicate Logic||DS2, November 4, 2015 in APB E005||File|
|Exercise||Test Exam Inspection||DS4, November 5, 2015 in APB E005|
|Exercise||Tutorial - Compactness Theorem||DS5, November 6, 2015 in APB E005|
|Lecture||Lecture - till Lemma 4.25||DS6, November 9, 2015 in APB E005||File|
|Lecture||Lecture - till slide 55||DS2, November 11, 2015 in APB E005|
|Exercise||Tutorial - Natural Deduction||DS4, November 12, 2015 in APB E005|
|Exercise||Tutorial - Completeness of Resolution, Pure Literals||DS5, November 13, 2015 in APB E005||File|
|Lecture||Lecture - till slide 61||DS6, November 16, 2015 in APB E005||File|
|Exercise||Tutorial - Syntax and Semantics of FOL||DS4, November 19, 2015 in APB E005|
|Exercise||Tutorial||DS5, November 20, 2015 in APB E005|
|Lecture||Lecture - till Lemma 4.64||DS6, November 23, 2015 in APB E005||File|
|Lecture||Lecture||DS2, November 25, 2015 in APB E005|
|Exercise||Presentation of the European Partner Universities||DS4, November 26, 2015 in APB E005|
|Exercise||Tutorial - Herbrand Interpretation and Infinite Models||DS5, November 27, 2015 in APB E005|
|Exercise||Tutorial - Application of Prenex Normalform, Skolemization, Unification, Resolution and Factorization||DS4, December 3, 2015 in APB E005|
|Exercise||Tutorial||DS5, December 4, 2015 in APB E005|
|Exercise||Tutorial||DS4, December 10, 2015 in APB E005|
|Exercise||Tutorial||DS5, December 11, 2015 in APB E005|
|Exercise||Tutorial - Corresponding Herbrand Interpretations and General Q&A session||DS4, December 17, 2015 in APB E005|