Kurssi on esitietona kaikissa opintosuunnissa ja erityisesti
tietojenkäsittelyteorian pää- ja sivuaineissa. Kurssin aihepiirillä on
kytkentöjä esim. seuraaville kursseille:
|
SOVELTAMINEN |
YMMÄRTÄMINEN |
TIETÄMINEN |
Ydinaines |
Looginen kieli:
- loogiset väittämät (termit, atomiset kaavat, kaavat ja lauseet)
- konnektiivit
- presedenssisäännöt
- kvanttorien laajuus
- muuttujien sidonta
|
Totuusjakelut ja struktuurit |
Totuusmääritelmä ja mallin käsite |
Tietämyksen esittäminen: määritelmien kirjoittaminen |
Semanttinen taulu:
- käyttö loogisten probleemojen ratkaisemiseen
- vastaesimerkkien muodostaminen
|
Konjunktiivinen ja disjunktiivinen normaalimuoto, prenex-normaalimuoto:
muunnossäännöt, eksistenssikvanttorien eliminointi
|
Ohjelmien oikeellisuus:
- ehtolausekkeet
- esi- ja jälkiehdot
|
|
Loogiset peruskäsitteet:
- toteutuvuus
- pätevyys
- looginen seuraavuus ja ekvivalenssi
|
|
Semanttinen taulu:
- ominaisuudet (virheettömyys ja täydellisyys)
- systemaattinen taulu
|
Konjunktiivinen ja disjunktiivinen normaalimuoto: sievennysperiaatteita
|
|
|
Looginen kieli:
|
Klausuulimuoto |
Unifikaatio:
- substituutiot
- (yleisimmät) unifioijat
- unifikaatioalgoritmi
|
Loogisten probleemojen ratkaiseminen resoluutiolla |
Ohjelmien oikeellisuus:
- invariantit
- heikoimmat esiehdot
- osittaisen oikeellisuuden päättelysäännöt
|
|
Konnektiivien keskinäinen määriteltävyys |
Loogisten peruskäsitteiden väliset yhteydet |
Prenex-normaalimuoto: eksistenssikvanttorien eliminointi |
Laskennallinen vaativuus: keskeiset vaativuusluokat (P ja NP) |
|
Tietämyksen esittäminen: rekursion problematiikka |
Klassiset todistusjärjestelmät (Hilbert ja Suppes) |
Herbrandin teoreema:
- Herbrand-universumit
- Herbrand-struktuurit
- lause- ja predikaattilogiikan suhde
|
Resoluution virheettömyys ja täydellisyys |
|
|
|
Laskennallinen vaativuus:
- Turing-koneet
- päätösongelmat
|
|
Tietämyksen esittäminen:
- täydellisten määritelmien kirjoittaminen
- nimien yksikäsitteisyys ja kattavuus
| |
Tukijoukkostrategia resoluutiossa |
Laskennallinen vaativuus: reduktiot ja vaikeat ongelmat
(NP-täydellisyys) |
Ohjelmien täysi oikeellisuus |
|
Ylläolevassa taulukossa on luokiteltu kurssilla opetettavaa ainesta
kaksisuuntaisen mallin mukaisesti: