Materijali sa predavanja
- Tema 0: Uvod u automatsko
rezonovanje. Osnovne informacije o
predmetu.(slajdovi)
- Tema 1: Iskazna logika. Sintaksa i
semantika. Normalne forme. SAT rešavači. Metod rezolucije. DP
procedura. DPLL procedura. CDCL procedura. Metod tabloa. Teorema
kompaktnosti. Primene SAT rešavača (slajdovi,
primeri)
- Tema 2: Logika prvog reda. Sintaksa i
semantika. Normalne forme. Erbranova teorema i Gilmorova procedura.
Skolem-Lovenhajmova teorema i teorema kompaktnosti.
Unifikacija. Metod rezolucije u logici prvog reda. Metod tabloa.
Sistemi za dedukciju. Prirodna dedukcija.
(slajdovi,
primeri)
- Tema 3: Logika prvog reda sa jednakošću.
Normalne interpretacije. Aksiome jednakosti. Paramodulacija. Birkhofov
sistem. Kongruentno zatvorenje. Nelson-Openova procedura. Sistemi za
prezapisivanje termova. Zaustavljanje i konfluentnost. Uređenja prezapisivanja
i uređenja svođenja. Uređenja leksikografske staze. Knut-Bendiksova procedura
upotpunjavanja. (slajdovi,
primeri)
- Tema 4: Teorije prvog reda. Rezonovanje u teoriji.
Furije-Mockinova procedura. Simpleks metod. SMT rešavači.
(slajdovi,
primeri)
