Logika és informatikai alkalmazásai (tematika)
- Motivációs példák. Az ítéletkalkulus szintaxisa, szemantikája. Formalizálás ítéletkalkulusban.
- Logikai következmény és indirekt bizonyítás. Konjunktív normálformák, klózhalmazok, klózhalmazok megszorításai. A DPLL algoritmus.
- Rezolúció, különböző rezolúciós stratégiák, helyesség és teljesség.
- Tabló módszer, helyesség és teljesség.
- Elméletek és tulajdonságaik. Deduktív rendszerek: Gentzen és Hilbert rendszere.
- Hilbert rendszerének helyessége. A dedukciós tétel. Az ítéletkalkulus kompaktsági tétele, Az elsőrendű logika szintaxisa és szemantikája.
- Formalizálás elsőrendben. Kielégíthetetlenség szemantikus kifejtéssel. Elméletek elsőrendben, axiomatizálhatóság. CNF elsőrendben.
- Helyettesítés termekbe, formulákba. Normálformák elsőrendben: kiigazítás, prenex alak, Skolem alak.
- Zárt Skolem alak. Herbrand struktúrák, Herbrand tétele és következményei.
- Az elsőrendű logika kompaktsági tétele, Az alaprezolúciós algoritmus, helyesség és teljesség. Egyesítési algoritmus.
- Elsőrendű rezolúció. Helyesség és teljesség. A lift lemma.
- Logikai programozás, Prolog, Másodrendű logika.