Cilj kolegija Napredne formalne metode jest proširenje znanja stečenih u okviru kolegija Uvod u formalne metode. Proširenja obuhvaćaju proširenje logičkog računa s računa sudova na račun predikata prvog reda, kao i odgovarajuće proširenje pravila rezolucije. Proširenje jezika omogućuje bitno veće izražajne mogućnosti računa predikata u modeliranju problema, a prošireno pravilo rezolucije omogućuje njihovo mehaničko (kroz implementacije u odgovarajućim jezicima i alatima) rješavanje. Pravilo rezolucije za račun predikata prvog reda postaje osnovom deduktivnih mehanizama logičkih programskih jezika, počevši od Prologa kao temeljnog jezika logičkog programiranja pa do logičkih programskih jezika za rukovanje ograničenjima, u rasponu od jezika opće namjene, kao što je CHR (Constraint Handling Rules), do jezika za vrlo važne specifične potrebe modeliranja ograničenja vezanih za klase, objekte, atribute, poslovna pravila (kao što je OCL-Object Constraint Language) u sklopu programskih okruženja za “grafičko” modeliranje i projektiranje informacijskih sustava, kao što je Eclipse. U dijelu izlaganja studenti se upoznavaju s osnovama F-logike, kao proširenja računa predikata prvog reda, koje već ima, a u budućnosti će imati sve više važnih primjena (brzo prototipiranje aplikacija zbog inherentne mogućnosti metaprogramiranja, primjene u domeni sematičkog Weba, itd.).