T-79.5102 Laskennallisen logiikan erikoiskurssi (4 op) L V

Syksy 2005

Logiikkaan perustuvien menetelmien käyttö tietojenkäsittelyssä on lisääntynyt merkittävästi aivan viime vuosina. Tämän kehityksen taustalla ovat uudet toteutusmenetelmät loogiselle päättelylle, jotka yhdessä tietokoneiden kasvaneen suorituskyvyn kanssa ovat mahdollistaneet menetelmille aivan uudentyyppiä sovelluksia. Esimerkkeinä näistä mainittakoon digitaalipiirien verifointityökalut, automaattinen tuotekonfigurointi ja erilaiset rajoiteohjelmointisovellukset. Kurssilla tutustutuaan lauselogiikan parhaisiin toteutusmenetelmiin:

• binääriset päätöspuut,
• Davis-Putnam perusalgoritmi ja sen heuristiset muunnelmat sekä
• epätäydelliset stokastiset hakumenetelmät;

ja tietämystekniikassa käytettävään sääntöpohjaiseen päättelyyn:

• stabiileihin malleihin perustuva semantiikka,
• approksimoiva päättely,
• stabiilien mallien laskenta branch and bound -tyyppisellä haulla sekä
• ilmaisuvoimaero lauselogiikkaan nähden.

Kurssi koostuu luennoista, laskuharjoituksista sekä kotitehtävistä, joissa tutustutaan käsiteltyihin menetelmiin perustuviin työkaluihin. Kotitehtävien aiheena ovat digitaalipiirien verifiointi ja suunnitteluongelman esittäminen sekä lauselogiikan toteutuvuusongelmana että stabiilien mallien hakuongelmana. Kurssi suoritetaan tekemällä kotitehtävät ja tentti. Kurssi on soveltuu kaikille formaaleista menetelmistä kiinnostuneille ja se on jatko-opintokelpoinen.

• Kirjallisuus: Luentomonisteet. Artikkeleita.
• Luennot: maanantaisin klo 12-14, sali TB353; kurssi alkaa 12.9.2005.
• Laskuharjoitukset: tiistaisin klo 15-16, sali TB353
• Vastaava opettaja: Ma. prof., TkT Tomi Janhunen, sähköposti Tomi.Janhunentkk.fi, kotisivu http://www.tcs.hut.fi/~ttj/
• Assistentti: DI Emilia Oikarinen, sähköposti eoikarintcs.hut.fi, kotisivu http://www.tcs.hut.fi/~eoikarin/
• Esitiedot: T-79.3001 Logiikka tietotekniikassa: perusteet
• Kurssin kotisivu: http://www.tcs.hut.fi/Studies/T-79.5102/