1. komponenta

Vrsta nastave	Ukupno
Predavanja	30
Auditorne vježbe	15

* Opterećenje je izraženo u školskim satima (1 školski sat = 45 minuta)

CILJ KOLEGIJA: Stjecanje uvida u neke aspekte matematičke logike koji neposredno sudjeluju u suvremenoj softverskoj tehnologiji.

NASTAVNI SADRŽAJI:
1. Dokazivanje u računu sudova i predikata. Rezolucija i dijagrami odluke za račun sudova. Rezolucija za račun predikata. Herbrandov teorem. SLD-rezolucija i logičko programiranje, Prolog. Testovi valjanosti (semantički tabloi).
2. Temporalna logika i verifikacija modela. Temporalne formule i njihova semantika. Kripkeovi modeli i tranzicijski sustavi. Pravednost, sigurnost i živost u distribuiranim sustavima. Testovi valjanosti za LTL. Izražajnost LTL. Drugi modeli vremena: CTL, CTL*. Algoritmi verifikacije modela za LTL i CTL*. Apstrakcija stanja i simbolička verifikacija modela. Interpretacije u automatima. Verifikacija modela u razvoju softvera - postupci i alati.
3. Druge modalne logike u računarstvu. Logike akcija i programa, dinamička logika. Hoareove trojke i verifikacija programa. Logike znanja i očekivanja. Zajedničko i opće znanje. Modeliranje i verifikacija pomoću KT45n.

OBAVEZE STUDENATA TOKOM NASTAVE I NAČINI NJIHOVA IZVRŠAVANJA: Pohađanje predavanja i vježbi, izrada domaćih zadaća, polaganje dva kolokvija.

UVJETI ZA POTPIS: Prisustvo na 70% predavanja i vježbi, predaja rješenja za 70% domaćih zadaća, prolazna ocjena na svim kolokvijima.

NAČIN POLAGANJA ISPITA: Završni dio ispita polaže se u pismenom ili usmenom obliku. Konačna ocjena oblikuje se na osnovi uspjeha u izradi domaćih zadaća, ocjena dobivenih na kolokvijima te ocjene odgovora na završnom dijelu ispita.

1. Mathematical Logic for Computer Science, M. Ben-Ari, Springer Verlag, 2001.
2. Logic in Computer Science, M. Huth, M. Ryan, Cambridge University Press, 2004.
3. Model-Checking, E. M. Clarke, O. Grumberg, D. A. Peled, MIT Press, 2000.
4. The Temporal Logic of Reactive and Concurrent Systems, Z. Manna, A. Pnueli, Springer Verlag, 1991.
5. Reasoning about Knowledge, R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi, MIT Press, 2003.
6. Modal Logic, P. Blackburn, M. de Riejke, Y. de Venema, Cambridge University Press, 2002.
7. Systems and Software Verification, B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, Springer Verlag, 2001.
8. Matematička logika, M. Vuković, Element, Zagreb, 2009.

Izborni predmet 3, 4, 5, 6 - Redovni Studij - Računarstvo i matematika

Izborni predmet 3, 4, 5, 6 - Redovni Studij - Računarstvo i matematika