Sammanfattning vecka 1 av lektion och övning:
- allmänt om kursen, lärandemål, tentamen, kursbok, läsanvisningar i kurs-PM, alternativ litteratur
- lite historia om logik, dess roll i filosofi, automatiska resonemang, AI och i datavetenskap
Logik var från början ett sätt att hantera kunskap och strukturera resonemang.
Numera ligger fokus på formella bevis i matematik och på mekaniska (datorbaserade) resonemang.
I filosofisk logik studerar man bevissystem. Vilken styrka har de? Vad kan man bevisa?
Hur hanterar man paradoxer och obevisbara satser? Är det skillnad på sanning och bevisbarhet?
Hur kan man försvara ett resonemang?
Vad vet vi. Vilka satser har entydiga sanningsvärden ("sann" T, eller "falskt" F)=
- Satslogik/"propositional logic" (Boolesk logik, sanningstabeller,
konnektiven och deras sanningstabeller
konjunktion ("och", "&", "^", ",")
disjunktion ("eller","or", "v", ";"),
implikation ("om", "->", "<-", ":-"),
ekvivalens ("om och endast om","omm", "<->"),
negation ("icke", "not", "\+")
- Predikatlogik
logiska variabler
kvantifikatorer, "för alla", "existerar"
scoperegler i predikat.
Bevisregler uttryckta med naturlig deduktion. ("natural deduction")
- Logikprogrammering: Att använda konstruktion av logiska bevis som programmeringsspråk
Enkla Prologprogram.
En familjedatabas.(hemuppgift att definiera några familjerelationer).
Vilka data finns i Prolog? konstanter och sammansatta termer
Syntaxen för Prologsatser
- Abstrakt beskrivning av exekveringen av Prologprogram
Likhetsteorin, vad är "substitutioner" (i beskrivningen)
Resultatet av en exekvering är svaret "yes" eller "no"
Vid "yes" levereras bindningar för de obundna variabler som ingår i frågan, en del av
en substitution som vi kallar "bindningsomgivningen". Detta kan uppfattas som ett antal villkor:
("jag har tagit fram ett bevis av påståendet och antagit att dessa variabler har dessa värden ").
Hur unifieringsalgoritmen som sköter detta fungerar och vad program "betyder" deklarativt ("modellteorin") tar vi nästa gång.
Hälsningar -Thomas