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.

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

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