FOI Nastava - Uvod u formalne metode

Sadržaj se učitava...

FOI Nastava

apps

mdi-login

Uvod u formalne metode

Introduction to Formal Methods
2024/2025

5 ECTSa

Katedra za teorijske i primijenjene osnove informacijskih znanosti

. 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

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 Seminar	1 2	1 2	1 1
Sekovanić Vlatka	Suradnik	Seminar	5	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 i primijeniti matematičke metode, modele i tehnike primjerene rješavanju problema iz područja informacijskih i poslovnih sustava
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
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

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

U kalendaru ispod se nalaze konzultacije predmetnih nastavnika, no za detalje o konzultacijama možete provjeriti na profilu pojedinog predmetnog nastavnika.