T-79.144 Logiikka tietotekniikassa: perusteet

Ydinainesanalyysi

Tämän sivun sisältö on valikoitu aiemmin syksyllä 2004 suoritetusta ydinainesanalyysistä, jota on tehty Tietotekniikan osastolla.

Esitietovaatimukset

Kurssilla on seuraavat esitietovaatimukset:

Kurssi on esitietona kaikissa opintosuunnissa ja erityisesti tietojenkäsittelyteorian pää- ja sivuaineissa. Kurssin aihepiirillä on kytkentöjä esim. seuraaville kursseille:

Oppimistavoitteet

Kurssin suorittamisella hankittavat keskeiset tiedot ja taidot:

Ydinainesanalyysitaulukko

(Versio 8.12.2004)

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
Täydentävä
tietämys
Looginen kieli:
  • jäsennyspuut
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
Erityis-
tietämys
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:

Minimiedellytykset

Kurssin suorittaminen arvosanalla 1 edellyttää seuraavien asioiden hallintaa:
Tomi Janhunen