FOI Nastava - Uvod u formalne metode

Sadržaj se učitava...

FOI Nastava

apps

mdi-login

Uvod u formalne metode

Introduction to Formal Methods
2023/2024

5 ECTSa

Informacijski i poslovni sustavi 1.1 (PDS)

Katedra za teorijske i primijenjene osnove informacijskih znanosti

5. 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)	Poslovni sustavi	5	izborni
Informacijski i poslovni sustavi 1.1 (PDS)	Informacijski 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	Seminar	3	2	1
Sekovanić Vlatka	Suradnik	Seminar Seminar	4 1	2 1	1 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.