Materijali sa predavanja
- Tema 0: Uvod u automatsko
rezonovanje. Osnovne informacije o
predmetu.(slajdovi)
- Tema 1: Iskazna logika. Sintaksa i
semantika. Normalne forme. Odlučivost iskazne logike. Kompaktnost. (slajdovi)
- Tema 2: Rezonovanje u iskaznoj logici. Metod tabloa. SAT problem i SAT rešavači.
Metod rezolucije. DPLL procedura. CDCL procedura. (slajdovi,
primeri)
- Tema 3: Logika prvog reda. Sintaksa i
semantika. Normalne forme. Neodlučivost logike prvog reda. Erbranova teorema.
Skolem-Lovenhajmova teorema i teorema kompaktnosti.
(slajdovi)
- Tema 4: Rezonovanje u logici prvog reda. Metod tabloa. Metode zasnovane
na Erbranovoj teoremi. Gilmorova procedura.
Unifikacija. Metod rezolucije u logici prvog reda.
(slajdovi)
- Tema 5: Sistemi za dedukciju. Prirodna dedukcija. (slajdovi,
primeri)
- Tema 6: Rezonovanje sa jednakošću.
Normalne interpretacije. Aksiome jednakosti. Paramodulacija. Birkhofov
sistem. Kongruentno zatvorenje. Nelson-Openova procedura. Sistemi za
prezapisivanje termova. (slajdovi,
primeri)
- Tema 7: Teorije prvog reda. Rezonovanje u teoriji.
Furije-Mockinova procedura. Simpleks metod. SMT rešavači.
(slajdovi,
primeri)
