Az informatika logika alapjai

Informatika
Eszterházy Károly Katolikus Egyetem
3 kredit

Oktatók: Kovásznai Gergely, Kusper Gábor, Bíró Csaba

Jelentkezz!

A kurzushoz nincs felvehető időpont. Nézz vissza később!

Lezárt időpontok

2019/20/1
Magyar
22 September 20195 January 2020
9 September 2019
 – 
29 September 2019
2018/19/2
Magyar
24 February 20192 June 2019
10 February 2019
 – 
25 February 2019
2018/19/1
Magyar
23 September 201821 December 2018
9 September 2018
 – 
26 September 2018
2017/18/2
Magyar
21 February 201827 May 2018
4 February 2018
 – 
20 February 2018
2017/18/1
Magyar
15 September 201716 December 2017
3 September 2017
 – 
24 September 2017

Kedvcsináló

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.

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.
Létrehozva: 2017. 01. 26, utoljára módosítva: 2020. 02. 15.