• Osnovna literatura
• Parser!!
• Sa časova vežbi
• Zadaci za pripremu kolokvijuma!!
• Teme za seminarske radove!!
• Kolokvijum -- rezultati!!
• VAŽNO!!Zadaci za pripremu ispita!!
• Dodatni materijali i linkovi

• John Harrison. Handbook of Practical Logic and Automated Reasoning.
• Predrag Janičić. Matematička logika u računarstvu.
• Franz Baader, Tobias Nipkow. Term rewriting and all that.
• Filip Marić. Beleške sa predavanja (i širi spisak literature)
• C++ literatura

Parser za iskaznu logiku i logiku prvog reda možete preuzeti ovde.

• Tročas I (19. 2. 2013.): Upoznavanje sa kursom. Sintaksa i semantika iskazne logike. (1.cpp).
• Tročas II (26. 2. 2013.): Sintaksa i semantika iskazne logike. Normalne forme. (2.cpp).
• Tročas III (5. 3. 2013.): Cajtinova transformacija. SAT problem i SAT rešavači. DIMACS format. Metod istinitosnih tablica. DPLL procedura. (dpll.cpp, truth_table.cpp, test-SAT.cnf, test-UNSAT.cnf). Svi primeri: 3.zip
• Tročas IV (12. 3. 2013.): Primene SAT rešavača. (4.zip)
• Tročas V (19. 3. 2013.): Prirodna dedukcija u sistemu Isabelle. (primeri).
• Tročas VI (26. 3. 2013.): Sintaksa i semantika logike prvog reda. (6.cpp). Svi primeri: 6.zip
• Tročas VII (2. 4. 2013.): Normalne forme u logici prvog reda. PRENEX. Skolemizacija. (7.cpp). Svi primeri: 7.zip
• Tročas VII (9. 4. 2013.): Unifikacija. Rezolucija. (8.cpp). Svi primeri: 8.zip
• Tročas IX (16. 4. 2013.): Rezolucioni rešavači. Vampire. TPTP format. (9.zip)
• Tročas X (7. 5. 2013.): Jednakosno rezonovanje. Kongruentna zatvorenja. Nelson-Open-ov algoritam. Prezapisivanje. (10.zip)
• Tročas XI (14. 5. 2013.): Zadovoljivost u odnosu na teoriju (SMT). (11.zip)

Zadaci za pripremu kolokvijuma mogu se preuzeti ovde.

Teme za seminarske radove možete pogledati na ovoj strani. Svaku temu rade dva studenta u paru. Prijave slati isključivo na mejl predmetnog asistenta. Teme će biti dodeljivane onim redom kojim se studenti budu prijavljivali. Studenti mogu predložiti i neku temu koja nije na spisku, ako ista ima smisla, biće uzeta u razmatranje. Seminarski se brani kod profesora. Za detalje o izradi seminarskog rada, obratiti se profesoru.

Na ovoj strani možete videti koje su teme do sada zauzete, a koje su slobodne.

Rezultati kolokvijuma mogu se videti na ovoj strani.

Zadaci za pripremu ispita mogu se preuzeti ovde.

• C++ vežbe (Saša Malkov, 2001-2006)
• Saša Malkov, Razvoj Softvera, C++
• MINISAT SAT rešavač
• YICES SMT rešavač
• CVC3 SMT rešavač
• MathSAT SMT rešavač
• Z3 SMT rešavač
• BarelogicTools SMT rešavač
• Vampire rezolucioni rešavač
• SMT-LIB 1.2 standard
• TPTP format