CS 2800: Kevät 2019

Kurssilla tutustutaan muodolliseen logiikkaan ja sen syviin yhteyksiin tietojenkäsittelyyn. Logiikka esitellään laskennallisesta näkökulmasta käyttäen ACL2 Sedantheorem proving -järjestelmää. Kurssin tavoitteena on esitelläfundamentaaliset, perustavanlaatuiset menetelmät laskennan mallintamiseen, suunnitteluun ja päättelyyn, mukaan lukien propositionaalinen logiikka, rekursio, induktio, yhtäläinen päättely, terminaatioanalyysi, uudelleenkirjoittaminen ja erilaiset todistustekniikat. Näytämme, miten logiikan avulla voidaan formalisoida ACL2s-kielen, joka on yksinkertainen LISP-pohjainen kieli, jossa on sopimuksia, syntaksi ja semantiikka. Sen jälkeen käytämmeACL2s-kieltä muodolliseen päättelyyn ohjelmista, eri abstraktiotasojen järjestelmien mallintamiseen, järjestelmien välisten rajapintojen suunnitteluun ja määrittelyyn sekä tällaisten koostettujen järjestelmien päättelyyn. Tarkastelemme myös päätösproseduureja ensimmäisen kertaluvun logiikan pirstaleille ja sitä, miten tällaisia päätösproseduureja voidaan käyttää järjestelmien mallien analysointiin.

Edellytyksenä on perehtyneisyys funktionaaliseen ohjelmointiin (CS 2500) ja diskreetteihin rakenteisiin (CS 1800). Jos sinulla ei ole tätä taustaa, tarvitset opettajan luvan.

Kurssille osallistuvien opiskelijoiden on tarkistettava Piazza-palvelun ilmoitukset päivittäin.