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. M. Ben-Ari: Mathematical Logic for Computer Science
2. M. Huth, M. Ryan: Logic in Computer Science
3. E. M. Clarke, O. Grumberg, D. A. Peled: Model-Checking
4. Z. Manna, A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems
5. R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi: Reasoning about Knowledge
6. P. Blackburn, M. de Riejke, Y. de Venema: Modal Logic
7. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen: Systems and Software Verification
8. M. Vuković: Matematička logika

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

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