TIEA3810 Sovellettu predikaattilogiikka (5 op)

Abstrakti ja konkreettinen syntaksi, BNF. Lausekepuut. Ensimmäisen kertaluvun kieli, tulkinta ja malli. Täsmällisten väittämien ilmaiseminen predikaattilogiikalla. Käytännön päättelysääntöjä. Tietokoneohjelmista päätteleminen. Pikakatsaus täydellisyys- ja epätäydellisyyslauseisiin.

Kurssin suorittamisen jälkeen opiskelija

* osaa tulkita BNF:llä esitettyjä syntaksikuvauksia

* hallitsee abstraktin ja konkreettisen syntaksin välisen eron

* tiedostaa, että sama informaatiosisältö voidaan esittää eri syntakseilla

* hallitsee lausekkeen ja lausekepuun yhteyden sekä sulkujen ja sitovuussääntöjen vaikutuksen

* tunnistaa vapaat ja sidotut muuttujien esiintymät sekä avoimet ja suljetut kaavat

* tietää miten ensimmäisen kertaluvun kaavan totuusarvo määräytyy

* osaa esittää ja tulkita tietokoneohjelman tilaa koskevia väittämiä

* hallitsee käytännöllisiä päättelysääntöjä, kuten de Morganin lait, Boolen laajennoslauseen ja kvanttoreita koskevia lakeja

* osaa tehdä yksinkertaisia päättelyketjuja ensimmäisen kertaluvun logiikassa

* ymmärtää Gödelin täydellisyyslauseen ja 1. epätäydellisyyslauseen, Church-Turingin teesin sekä pysähtymistesterin olemattomuuslauseen sisällön

Kurssilla suhteutetaan logiikan käsitteistöä ohjelmoinnin käsitteistöön ja käytetään esimerkkejä tietokokoneohjelmien maailmasta. Pysähtymistesterin olemattomuus todistetaan, mutta Gödelin täydellisyyslausetta jne. ei. Propositiologiikan merkinnät ja todistaminen arkimatematiikassa ovat esitietokursseilla.