Grundläggande logik och modellteori (HT-14)

Kursöversikt och läsanvisningar

Litteratur

Alla kapitel- och uppgiftsnummer nedan hänvisar till Mordechai Ben-Ari, Mathematical Logic for Computer Science, andra resp. tredje upplagan.

Kapitel och övningar inom parentes är av intresse för den som vill ha en djupare förståelse för materialet, men inte strikt nödvändiga för att uppnå kursens lärmål.

Översikt

Notera att nedanstående är en preliminär planering som kan komma att ändras under kursens gång.

Föreläsning Innehåll Kapitel (2. uppl.) Uppgifter (2. uppl.) Kapitel (3. uppl.) Uppgifter (3. uppl.)
1 (1/9) Introduktion, satslogik 1, 2.1-2.3 1.1 1, 2.1-2.3 1.1
2 (4/9) Satslogik 2.4-2.6, (2.7, 2.8) 2.1, (2.2,2.3), 2.4-2.5, (2.6-2.10), 2.12 2.4-2.6, (2.7), 2.8 2.1, (2.2), 2.3-2.9, (2.11), 2.13
3 (11/9) Bevissystem, Hilbertsystem 3.1-3.3, (3.4) (3.1-3.3), 3.4-3.7, 3.11 3.1-3.4, (3.5), 3.10 (3.1-3.3), 3.4,3.5,3.7-3.9, 3.14
4 (15/9) Konjunktiv och disjunktiv normalform 4.1 4.1,4.2 4.1-4.2 4.1,4.2
5 (18/9) Resolution 4.4,4.6 4.3, (4.4), 4.5 4.3-4.5
6 (22/9) Binära beslutsdiagram (BDD) 4.2 5.1-5.4, (5.5), 5.7 5.1-5.3
7 (29/9) SAT och SAT-lösare. Predikatlogik 6.1-6.3, (6.4)
8 (2/10) Predikatlogik 5.1-5.4, (5.5) 5.1-5.7 7.1-7.4, (7.5), 7.7 7.1-7.8, (7.9)
9 (6/10) Predikatlogiska normalformer 7.1-7.2 7.1,7.4 9.1-9.2 TBA
10 (9/10) Predikatlogisk unifiering 7.6-7.7 7.6,(7.7),7.8 10.1-10.3 10.2, (10.3), 10.4
11 (13/10) Predikatlogisk resolution 7.8 7.10 10.4, (10.5),10.6 10.10
12 (17/10) Logikprogrammering 8.1-8.3 8.3 11.1-11.6 11.2
13 (20/10) Temporallogik TBA TBA TBA TBA
14 (23/10) Temporallogik TBA TBA TBA TBA