Az informatika logika alapjai

Informatika
Eszterházy Károly Tudományegyetem
Oktatók: Kovásznai Gergely, Kusper Gábor, Bíró Csaba
Megszerezhető kredit: 3

Leírás

Hogyan tudjuk a mindennapi életből merített problémákat, természetes nyelven kimondott állításokat megfelelő módon, logikai úton modellezni? Ki tudjuk-e a kapott logikai állításokat értékelni és a logikai következtetésekkel kapcsolatos kérdéseket megválaszolni?

Fontos, hogy a hallgatók a megismerjék a logikus gondolkodással kapcsolatos fogalmakat, a gyakorlatban és a programozási feladatokban tudják alkalmazni azokat. Mindez fontos alapot nyújt ahhoz, hogy a gyakorlati életben – akár szoftverfejlesztőként – a logikai problémákat sikeresen legyenek képesek interpretálni és megoldani, illetve alkalmazni a - cégek által is alkalmazott - standard formátumokat és tool-okat.

Léteznek-e algoritmusok a logikai következtetések elvégzésére? Ha igen, akkor ezeket le is tudnánk programozni? Esetleg már léteznek ilyen célú szoftverek? Hogyan tudjuk ezeket használni és pontosan milyen feladatokra is?

A hardver- és szoftvergyártó cégek is használnak a termékeik "verifikálására" ilyen szoftvereket? Hogyan történik egy mikrochip vagy egy forráskódrészlet verifikálása?

Követelmények:

A kurzus teljesítéséhez a hallgatóknak meg kell oldaniuk a modulzáró teszteket. Félév végén egy a tanárokkal egyeztetett személyes vagy skype beszélgetés keretében kell a megszerzett tudásukról számot adniuk.

Tanmenet

  1. Szövegértés és logika. A matematikai logika szerepe. Formalizálás 0. rendű logikában. Szintaktikai fogalmak. A logikai összekötő jelek szemantikája.
  2. "0." rendű logika szemantikai fogalmai: interpretáció (kiértékelés), logikai törvény, logikai ellentmondás, kielégíthetőség, logikai következmény. Igazságtábla. Bevezetés egy ingyenes komputeralgebrai rendszer használatába (Maxima, Wolfram Alpha live).
  3. Normálformák. KNF, DNF. Normálformára hozó algoritmusok.
  4. Programozás technikai vonatkozások (pl. ciklusba lépés, ciklusban maradás feltétele, feltételek elemzése, egyszerűsítése).
  5. Rezolúciós algoritmus 0. rendű logika esetén. DPLL algoritmus. Unit propagáció szabálya. Konfliktusok elemzése, klózok tanulása.
  6. SAT solving. DIMACS formátum. Létező SAT szolverek.
  7. SMT alapok, SAT-SMT összehasonlítása, egyszerűbb problémák (egész aritmetika) megfogalmazása. Létező SMT szolverek.
  8. "1." rendű logika bevezetése. Szövegértés és formalizálás 1. rendű logikában. Kvantorok szemantikája, értelmezésük ciklusként. 1. rendű logika szintaktikai fogalmai.
  9. Kvantorok hatásköre. Kötött és szabad változó-előfordulások. Formula paraméterei. 1. rendű logika szemantikai fogalmai.
  10. Normálformák. KNF. Prenex normálforma. Skolemizálás.
  11. Rezolúciós algoritmus 1. rendű logika esetén. Unifikáció.
  12. Bizonyítás rezolúció segítségével, teljes és nem teljes rezolúciós stratégiák, a lineáris és az input rezolúció.
  13. A Prolog szintaxisa, tények, szabályok, cél, Prolog program átírása Horn-klózok halmazává, az SLD-rezolució. Programozás a Prologban.

Időpontok

2019. szeptember 23. -2020. január 5.
2019. szept 9., hét 17:35
2019. szept 29., vas 23:00
Kurzus indítása
2019. február 25. -2019. június 2.
2019. feb 10., vas 21:21
2019. feb 25., hét 23:00
Kurzus indítása
2018. szeptember 24. -2018. december 22.
2018. szept 10., hét 0:00
2018. szept 26., sze 23:00
Kurzus indítása
2018. február 22. -2018. május 27.
2018. feb 5., hét 0:00
2018. feb 20., kedd 23:59
Kurzus indítása
2017. szeptember 16. -2017. december 16.
2017. szept 4., hét 0:00
2017. szept 24., vas 23:00
Kurzus indítása