Matematisk logik HT 98
Kursen ger en introduktion till logik. Två viktiga mål med kursen är
att
- förstå vad ett bevis är
- lära känna ett formellt bevissystem
Vi kommer att behandla sats- och predikatlogik och göra bevis
i ett formellt system som kallas naturlig deduktion. En rad egenskaper
hos sats- och predikatlogik kommer att visas; bl a fullständighet
vilket visar att ett påstående är en logisk sanning om och endast om
den går att bevisa i naturlig deduktion.
Laborationer
Vi kommer att använda beviseditorn
Alfa, i
vilken man kan göra bevis i naturlig deduktion på dator.
Alfa använder sig av
beviskontrolleraren
Agda,
som också har ett
emacsgränssnitt.
Det kommer att bli två
laborationer, en i satslogik och en i predikatlogik. Dessutom planeras
en mer avancerad laboration i vilken ett mer omfattande bevis skall
utvecklas i Agda; denna laboration är tänkt att ge bonus för betyget VG på
kursen.
Kursbok
Logic and Structure, författad av Dirk van Dalen och utgiven på
Springer. Kursen omfattar de två första kapitlen samt delar ur
kapitlen 3 och 5.
Omtenta
Torsdag 8/4 8.45-13.45. Lokal: VV . Bonuspoäng får tillgodoräknas även på
denna omtenta.
EXTRA FÖRELÄSNING INFÖR OMTENTAN
Den ordinarie tentan kommer att gås igenom fredagen den 26/3
kl. 13.15.
Lokal:
S4 (rum 2306), MC.
Jan Smith (kursansvarig)
Peter Bohlin(cl5pbohl@cs.chalmers.se) och Sebastian Sandberg(sebsand@math.chalmers.se)