| Semester: | Sommersemester 2013 |
| Veranstalter: | Prof. Giesl
|
| Bemerkungen: |
|
-
-
1. Introduction
- Fr, 12.04.2013, 10:00 Uhr
- Prolog, Facts and Rules, automated theorem proving, SLD trees
-
-
2 Foundations of Predicate Logic, 2.1 Syntax of Predicate Logic
- Mo, 15.04.2013, 15:45 Uhr
-
-
2.2 Semantics of Predicate Logic
- Fr, 19.04.2013, 10:00 Uhr
-
-
3 Resolution, 3.1 Skolem NF
- Mo, 22.04.2013, 15:45 Uhr
-
-
3.2 Herbrand Structures, Algorithm of Gilmore
- Fr, 26.04.2013, 10:00 Uhr
-
-
3.3 Ground Resolution
- Mo, 29.04.2013, 15:45 Uhr
-
-
3.3 Ground Resolution: Proof, Algorithm of Gilmore improved
3.4 Resolution for Predicate Logic and Unification
- Fr, 03.05.2013, 10:00 Uhr
- ..., Most General Unifier
-
-
3.4 Unification Algorithm
- Mo, 06.05.2013, 15:45 Uhr
- ..., Example 3.4.6, Lemma 3.4.8, ...
-
-
3.4 continued (Lifting Lemma)
3.5 Restrictions of Resolution
3.5.1 Linear Resolution
3.5.2 Input and SLD Resolution
- Fr, 10.05.2013, 10:00 Uhr
-
-
3.5.2 ... Horn clauses, SLD Resolution
4 Logic Programs
4.1 Syntax and Semantics of LPs
- Mo, 13.05.2013, 15:45 Uhr
-
-
4.1.1 Declarative Semantics
4.1.2 Procedural Semantics
4.1.3 Fixpoint Semantics of LP
- Fr, 17.05.2013, 10:00 Uhr
-
-
4.1.3 Fixpoint Semantics of LP
- Mo, 27.05.2013, 15:45 Uhr
-
-
4.2 Universality of LP
- Mo, 03.06.2013, 15:45 Uhr
-
-
4.2.5 Universality of LP
4.3 Indeterminisms and Evaluation Strategies
- Fr, 07.06.2013, 10:00 Uhr
- Proof of Theorem 4.2.5 continued
-
-
- Mo, 10.06.2013, 15:45 Uhr
-
- Fr, 14.06.2013, 10:00 Uhr
- Exercise instead of lecture
-
-
- Mo, 17.06.2013, 15:45 Uhr
-
-
- Fr, 21.06.2013, 10:00 Uhr
-
-
- Mo, 24.06.2013, 15:45 Uhr
-
-
- Fr, 28.06.2013, 10:00 Uhr
-
-
- Mo, 01.07.2013, 15:45 Uhr
-
-
- Fr, 05.07.2013, 10:00 Uhr