Sadržaj se učitava...
mdi-home Početna mdi-account-multiple Djelatnici mdi-script Studiji mdi-layers Katedre mdi-calendar-clock Raspored sati FOI Nastava search apps mdi-login
Uvod u formalne metode
Introduction to Formal Methods
2021/2022
5 ECTSa
Informacijski i poslovni sustavi 1.1 (PDS)
Katedra za teorijske i primijenjene osnove informacijskih znanosti
RI
3. semestar
 Osnovne informacijemdi-information-variant Izvođači nastavemdi-account-group Nastavni plan i programmdi-clipboard-text-outline Model praćenjamdi-human-male-board Ispitni rokovimdi-clipboard-check-outline Rasporedmdi-calendar-clock Konzultacijemdi-account-voice
Izvođenje kolegija
Studij Studijski program Semestar Obavezan
Informacijski i poslovni sustavi 1.1 (PDS) Informacijski sustavi 3 izborni
Informacijski i poslovni sustavi 1.1 (PDS) Informacijski sustavi 5 izborni
Informacijski i poslovni sustavi 1.1 (PDS) Poslovni sustavi 3 izborni
Informacijski i poslovni sustavi 1.1 (PDS) Poslovni sustavi 5 izborni
Cilj kolegija
Cilj kolegija Uvod u formalne metode je upoznavanje studenata s osnovnim metodama simboličke logike u primjeni na razvoj programske podrške, kako klasične, tako i suvremene. Studenti će usvojiti elemente sintakse i semantike klasičnog računa sudova, te metode automatske dedukcije, zasnovane na pravilu rezolucije za račun sudova i njegovim modifikacijama (semantička rezolucija, linearna rezolucija, hiperrzolucija), odnosno na metodi Davisa-Putnama. Usvojeni formalni jezik računa sudova i njegovih podsustava (Hornova logika) i nadsustava (kvantificirani računa sudova) i za njih razvijene metode automatske dedukcije zatim će poslužiti kao sredstvo modeliranja i rješavanja cijelog niza problema (kombinatornih, problema planiranja u umjetnoj inteligenciji, problema modeliranja strateških (šah) i kombinatornih (%22četiri u nizu%22) igara), te propozicijskih informacijskih i ekspertnih sustava.
Preduvjeti
Matematika 1 (PDS 1.1)
Norma kolegija
Predavanja
 30 sati
Seminar
 15 sati
Vježbe u praktikumu
 15 sati
Nastavnik Uloga na kolegiju Oblik nastave Tjedana Sati Grupa
Lovrenčić Sandra Nositelj Predavanja 7 2 1
Sekovanić Vlatka Suradnik Vježbe u praktikumu
Vježbe u praktikumu
Seminar 		1
7
15 		1
2
1 		2
2
1
Sadržaj predavanja
  •   Osnovni pojmovi, pregled sadržaja kolegija i literatura
    Nedostaje
  •   Opća struktura logičkih računa
    Gradivni elementi logičkih računa (jezik, skup “formula”, pravila logičkog izvoda). Gradivni elementi računa sudova (jezik, skup sudova).
  •   Pojam logičke posljedice za račun sudova i njegove karakaterizacije
    Pojam interpretacije suda. Semantičke tablice. Klasifikacija suda s obzirom na njegovu istinitost u svim svojim interpretacijama (tautologija, ispunjivi sud, kontradiktorni sud). Pojam logičke posljedice za račun sudova, definiran kao semantički pojam.
  •   Poučci o karakterizaciji pojma logičke posljedice za račun sudova
    Poučak koji kao osnovu za karakterizaciju koristi pojam tautologije. Poučak koji kao osnovu za karakterizaciju koristi pojam kontradiktornog suda.
  •   Primitivne normalne forme računa sudova. Pojmovi konjunkta i disjunkta
    Pojmovi konjunktivne i disjunktivne primitivne normalne forme. Procedura pretvaranja suda u ekvivalentnu konjunktivnu, odnosno disjunktivnu primitivnu normalnu formu.
  •   Svođenje problema logičke posljedice za račun sudova na problem ispitivanja kontradiktornosti pripadajućeg skupa disjunkta.
    Nedostaje
  •   Osnovno pravilo rezolucije za račun sudova
    Definicija i primjer. Valjanost pravila rezolucije za račun sudova kao pravila logičkog izvoda. Potpunost pravila rezolucije za račun sudova.
  •   Metoda zasićenja razina kao metoda sustavnog generiranja disjunkta i problem kombinatorne eksplozije
    Nedostaje
  •   Neke važnije modifikacije osnovnog pravila rezolucije za račun sudova (semantička rezolucija i linearna rezolucija)
    Nedostaje
  • Primjene pravila rezolucije na rješavanje problema logičkog izvoda
    Formaliziranje problema iskazanih govornim jezikom sredstvima računa sudova. Formalizacija principa golubinjaka i problema planiranja u domeni umjetne inteligencije. Ekspertni sustav nad domenom računa sudova (propozicijski ekspertni sustav).
  • Metoda Davisa-Putnama
    Motivacija metode Davisa-Putnama, njezina definicija skupom pravila izvoda i njezine primjene.
  • Hornov račun sudova
    Definicija Hornovih klauzula. Hornove klauzule kao gradivni elementi propozicijskih logičkih programa. Struktura propozicijskih logičkih programa. Deklarativna i proceduralna semantika propozicijskih logičkih programa
  • Opći problem ispunjivosti (SAT problem) i njegova složenost
    Nedostaje
  • Kvantificirani račun sudova
    Motivacija potrebe za kvantificiranim računom sudova. Ilustracija na primjerima modeliranja ranije modeliranih problema u nekvantificiranom (standardnom) računu sudova.
  • Propozicijske baze znanja. Aproksimacija (kompilacija) znanja u propozicijskoj bazi znanja.
    Nedostaje
  •   Osnovni pojmovi, pregled sadržaja kolegija i literatura
    Nedostaje
  •   Opća struktura logičkih računa
    Gradivni elementi logičkih računa (jezik, skup “formula”, pravila logičkog izvoda). Gradivni elementi računa sudova (jezik, skup sudova).
  •   Pojam logičke posljedice za račun sudova i njegove karakaterizacije
    Pojam interpretacije suda. Semantičke tablice. Klasifikacija suda s obzirom na njegovu istinitost u svim svojim interpretacijama (tautologija, ispunjivi sud, kontradiktorni sud). Pojam logičke posljedice za račun sudova, definiran kao semantički pojam.
  •   Poučci o karakterizaciji pojma logičke posljedice za račun sudova
    Poučak koji kao osnovu za karakterizaciju koristi pojam tautologije. Poučak koji kao osnovu za karakterizaciju koristi pojam kontradiktornog suda.
  •   Primitivne normalne forme računa sudova. Pojmovi konjunkta i disjunkta
    Pojmovi konjunktivne i disjunktivne primitivne normalne forme. Procedura pretvaranja suda u ekvivalentnu konjunktivnu, odnosno disjunktivnu primitivnu normalnu formu.
  •   Svođenje problema logičke posljedice za račun sudova na problem ispitivanja kontradiktornosti pripadajućeg skupa disjunkta.
    Nedostaje
  •   Osnovno pravilo rezolucije za račun sudova
    Definicija i primjer. Valjanost pravila rezolucije za račun sudova kao pravila logičkog izvoda. Potpunost pravila rezolucije za račun sudova.
  •   Metoda zasićenja razina kao metoda sustavnog generiranja disjunkta i problem kombinatorne eksplozije
    Nedostaje
  •   Neke važnije modifikacije osnovnog pravila rezolucije za račun sudova (semantička rezolucija i linearna rezolucija)
    Nedostaje
  • Primjene pravila rezolucije na rješavanje problema logičkog izvoda
    Formaliziranje problema iskazanih govornim jezikom sredstvima računa sudova. Formalizacija principa golubinjaka i problema planiranja u domeni umjetne inteligencije. Ekspertni sustav nad domenom računa sudova (propozicijski ekspertni sustav).
  • Metoda Davisa-Putnama
    Motivacija metode Davisa-Putnama, njezina definicija skupom pravila izvoda i njezine primjene.
  • Hornov račun sudova
    Definicija Hornovih klauzula. Hornove klauzule kao gradivni elementi propozicijskih logičkih programa. Struktura propozicijskih logičkih programa. Deklarativna i proceduralna semantika propozicijskih logičkih programa
  • Opći problem ispunjivosti (SAT problem) i njegova složenost
    Motivacija potrebe za kvantificiranim računom sudova. Ilustracija na primjerima modeliranja ranije modeliranih problema u nekvantificiranom (standardnom) računu sudova.
  • Kvantificirani račun sudova
    Nedostaje
  • Propozicijske baze znanja. Aproksimacija (kompilacija) znanja u propozicijskoj bazi znanja.
    Nedostaje
  •   Osnovni pojmovi, pregled sadržaja kolegija i literatura
    Nedostaje
  •   Opća struktura logičkih računa
    Gradivni elementi logičkih računa (jezik, skup “formula”, pravila logičkog izvoda). Gradivni elementi računa sudova (jezik, skup sudova).
  •   Pojam logičke posljedice za račun sudova i njegove karakaterizacije
    Pojam interpretacije suda. Semantičke tablice. Klasifikacija suda s obzirom na njegovu istinitost u svim svojim interpretacijama (tautologija, ispunjivi sud, kontradiktorni sud). Pojam logičke posljedice za račun sudova, definiran kao semantički pojam.
  •   Poučci o karakterizaciji pojma logičke posljedice za račun sudova
    Poučak koji kao osnovu za karakterizaciju koristi pojam tautologije. Poučak koji kao osnovu za karakterizaciju koristi pojam kontradiktornog suda.
  •   Primitivne normalne forme računa sudova. Pojmovi konjunkta i disjunkta
    Pojmovi konjunktivne i disjunktivne primitivne normalne forme. Procedura pretvaranja suda u ekvivalentnu konjunktivnu, odnosno disjunktivnu primitivnu normalnu formu.
  •   Svođenje problema logičke posljedice za račun sudova na problem ispitivanja kontradiktornosti pripadajućeg skupa disjunkta.
    Nedostaje
  •   Osnovno pravilo rezolucije za račun sudova
    Definicija i primjer. Valjanost pravila rezolucije za račun sudova kao pravila logičkog izvoda. Potpunost pravila rezolucije za račun sudova.
  •   Metoda zasićenja razina kao metoda sustavnog generiranja disjunkta i problem kombinatorne eksplozije
    Nedostaje
  •   Neke važnije modifikacije osnovnog pravila rezolucije za račun sudova (semantička rezolucija i linearna rezolucija)
    Nedostaje
  • Primjene pravila rezolucije na rješavanje problema logičkog izvoda
    Formaliziranje problema iskazanih govornim jezikom sredstvima računa sudova. Formalizacija principa golubinjaka i problema planiranja u domeni umjetne inteligencije. Ekspertni sustav nad domenom računa sudova (propozicijski ekspertni sustav).
  • Metoda Davisa-Putnama
    Motivacija metode Davisa-Putnama, njezina definicija skupom pravila izvoda i njezine primjene.
  • Hornov račun sudova
    Definicija Hornovih klauzula. Hornove klauzule kao gradivni elementi propozicijskih logičkih programa. Struktura propozicijskih logičkih programa. Deklarativna i proceduralna semantika propozicijskih logičkih programa
  • Opći problem ispunjivosti (SAT problem) i njegova složenost
    Nedostaje
  • Kvantificirani račun sudova
    Motivacija potrebe za kvantificiranim računom sudova. Ilustracija na primjerima modeliranja ranije modeliranih problema u nekvantificiranom (standardnom) računu sudova.
  • Propozicijske baze znanja. Aproksimacija (kompilacija) znanja u propozicijskoj bazi znanja.
    Nedostaje
 Sadržaj seminara/vježbi
  • 1. Prolog - uvod
    Povijest Prologa. Struktura Prolog programa – predikati i klauzule; činjenice, pravila i upiti. Hornova klauzula. Tipovi podataka – jednostavni objekti i strukture. Uvod u SWI-Prolog. Primjer unošenja činjenica. Jednostavni upiti – ispunjavanje ciljeva i usklađivanje. Primjer postavljanja jednostavnih upita.
  • 2. Prolog - upiti i pravila
    Opis rada jednostavnih upita i primjeri. Složeni upiti – više ciljeva. Opis rada složenih upita – backtracking. Grafički prikaz rada primjera različitih složenih upita. Ugrađeni predikati. Pravila – opis rada sa pravilima i primjeri.
  • 3. Prolog – aritmetika, upravljanje podacima i rekurzije
    Aritmetički izrazi u Prologu. Ugrađeni predikat is/2. Primjeri računskih operacija i uspoređivanja brojeva. Upravljanje podacima – predikati assert i retract. Direktiva dynamic/1. Primjeri pravila sa predikatima za upravljanje podacima. Rekurzivne klauzule – opis i način rada. Primjeri rekurzivnih klauzula.
  • 4. Prolog - zadatak 1
    Samostalno rješavanje zadatka u Prologu sa primjenom znanja naučenog na vježbama 1-3.
  • 5. Prolog - strukture i negacija
    Strukture – opis i primjeri. Upiti sa strukturama. Negacija u Prologu – pretpostavka zatvorenog svijeta i negacija kao neuspjeh. Ugrađeni predikat not/1. Primjeri pravila sa korištenjem negacije. Dodavanje negacije u zadatak sa prošlih vježbi.
  • 6. Prolog - operatori i rez
    Operatori u Prologu. Predefinirani operator op/3. Kreiranje vlastitih operatora. Kreiranje sučelja sa prirodnijim jezikom pomoću operatora. Primjer sa operatorima. Rez – isključivanje backtrackinga. Opis rada pravila sa rezom na različitim primjerima. Primjeri varijanti klauzula sa rezom i bez reza.
  • 7. Prolog – kontrolne strukture, sučelje i liste
    Kontrolne strukture u Prologu – if-then-else i repeat. Primjeri korištenja kontrolnih struktura. Kreiranje sučelja za pojedini program – primjer. Liste – opis i primjeri. Upiti sa listama. Specijalni zapis liste - pretraživanje, dodavanje i brisanje elemenata liste. Primjeri rada sa listama.
  • 8. Prolog - zadatak 2
    Samostalno rješavanje složenijeg zadatka u Prologu sa primjenom znanja naučenog na vježbama 1-7.
 Ishodi učenja kolegija
  • razumjeti i primijeniti ključne aspekte informacijske tehnologije (programiranje, algoritmi, strukture podataka, baze podataka i znanja)
  • ovladati idejnim postavkama i osnovnim tehnikama logičkog programiranja
  • razumjeti potrebu sustavnog i egzaktnog pristupa modeliranju i implementaciji informacijskih i poslovnih sustava te spoznati ulogu formalnih metoda (metoda simboličke logike) u tim procesima.
  • analizirati stanje, identificirati prilike i definirati probleme s kojima se susreću organizacije i pojedinci
  • analizirati stanje, identificirati prilike i definirati probleme s kojima se susreću organizacije i pojedinci u primjeni ICT, te formulirati rješenja uz primjenu ICT
  • raditi u timu za izgradnju informacijskih sustava
  • konceptualno i formalno modelirati različite segmente informacijskih i poslovnih sustava
 Ishodi učenja programa
  • razumjeti stanje i trendove razvoja suvremenih informacijskih i komunikacijskih tehnologija (ICT), razumjeti njihov utjecaj na pojedinca, organizaciju i društvo te procijeniti njihovu primjenjivost u zadanom kontekstu
  • razumjeti i primijeniti ključne aspekte informacijske tehnologije (programiranje, algoritmi, strukture podataka, baze podataka i znanja
  • razumjeti i primijeniti suvremene tehničke koncepte i prakse u informacijskim tehnologijama (arhitektura računala, operacijski sustavi, mreže računala)
  • razumjeti i primijeniti matematičke metode, modele i tehnike primjerene rješavanju problema iz područja informacijskih i poslovnih sustava
  • razumjeti bitne čimbenike koji utječu na poslovanje organizacije i pojedinaca te primijeniti osnovne metode i koncepte planiranja, upravljanja i obračuna poslovanja
  • analizirati stanje, identificirati prilike i definirati probleme s kojima se susreću organizacije i pojedinci u primjeni ICT, te formulirati rješenja uz primjenu ICT
  • razumjeti osnovna vertikalna područja primjene ICT (industrija, zdravstvo, promet, turizam, država i sl.), te horizontalne aplikacije (uredski sustavi, DSS, CRM, ERP, DMS i sl.)
  • razumjeti i primijeniti suvremene metodološke pristupe razvoja organizacijskih i informacijskih sustava, te oblikovanja organizacije i organizacijske strukture
  • razumjeti suvremene organizacijske koncepte i upravljati organizacijskom kulturom
  • modelirati poslovne procese i podatke u organizacijama i primijeniti modele u razvoju informacijskih i poslovnih sustava
  • razumjeti i primijeniti metode, tehnike razvoja informacijskih i programskih sustava u suvremenim razvojnim okolinama
  • razumjeti i primijeniti procese, metode i tehnologije upravljanja IT uslugama i resursima te podrške i pružanja različitih vrsta usluga vezanih uz ICT
  • razumjeti i primijeniti etička načela, zakonsku regulativu i norme koje se primjenjuju u struci
  • razumjeti osnovna načela i metode upravljanja organizacijom i uspješno raditi u timu
  • uspješno komunicirati s klijentima, korisnicima i kolegama na verbalan i pisani način uz primjenu odgovarajuće terminologije uključujući i sposobnost komunikacije o struci na stranom jeziku
  • pratiti stručnu literaturu na hrvatskom i stranom jeziku, pripremiti i samostalno održati prezentacije na hrvatskom i stranom jeziku stručnoj i općoj publici, te kritičku evaluaciju prezentirane stručne teme
  • razumjeti i primijeniti vještine učenja potrebne za cjeloživotno učenje i nastavak obrazovanja na diplomskom studiju
  • razumjeti i primijeniti osnovne principe planiranja i razvoja karijere u struci i vlastitih poduzetničkih poduhvata
  • poznavati ključne aspekte informacijske tehnologije
  • identificirati i razumjeti bitne čimbenike koji utječu na poslovanje organizacije i pojedinaca te primijeniti osnovne metode i koncepte planiranja, upravljanja i obračuna poslovanja
  • prepoznati osnovna vertikalna područja primjene ICT (industrija, zdravstvo, promet, turizam, država i sl.), te horizontalne aplikacije (uredski sustavi, DSS, CRM, ERP, DMS i sl.)
  • razumjeti metode, tehnike razvoja informacijskih i programskih sustava u suvremenim razvojnim okolinama
  • razumjeti procese, metode i tehnologije upravljanja IT uslugama i resursima te podrške i pružanja različitih vrsta usluga vezanih uz ICT
  • identificirati ključne podatke i informacije za donošenje racionalnih poslovnih odluka
  • analizirati i vrednovati rezultat poslovanja, te predložiti unapređenje poslovnog sustava.
  • PROBAnje OPISivanja....
 Osnovna literatura
  • Čubrilo, M. Matematička logika za ekspertne sisteme. Informator, Zagreb, 1989.
  • Truemper, K. Design of Logic-based Intelligent Systems. John Wiley and Sons, Hoboken, 2004.
 Dopunska literatura
  • Barwise, J.; Etchemendy, J. Language: proof and logic. CSLI publications, Stanford, 2008.
  • Jeroslow, R.G. Logic-based decision support. North-Holland, Amsterdam, 1989.
  • Bratko, I. Prolog programming for artificial intelligence. 3rd ed. Addison Wesley, Harlow, 2001.
 Slični kolegiji
  • Prema dostupnim podacima, ekvivalentnih predmeta na dodiplomskim studijima u Republici Hrvatskoj nema. Postoje donekle srodni predmeti tipa “Logičko programiranje” (Filozofski fakultet-Zagreb), “Matematička logika” (filozofski fakultet u Rijeci), “Matematička i moderna logika” (Filozofski fakultet Družbe Isusove-Zagreb), “Logika III” i “Logika IV” (Filozofski fakultet Zagreb), “Deskriptivna logika” (poslijediplomski doktorski studij, FER-Zagreb),…
 Redoviti studenti Izvanredni studenti
izvanredni rok
Datum: 14.04.2025.
Vrijeme: 16:00
Opis: Na Fakultetu
U kalendaru ispod se nalaze konzultacije predmetnih nastavnika, no za detalje o konzultacijama možete provjeriti na profilu pojedinog predmetnog nastavnika.
 2024 © Fakultet organizacije i informatike, Centar za razvoj programskih proizvoda