A formális logika modellezési eszközkészletének az alkalmazása - informatikus szemével nézve. Logikai következtetéseket végző algoritmusok bemutatása konkrét - ipari cégek által is használt - szoftvereken keresztül.

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.

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.