FOI Nastava - Napredne formalne metode

Sadržaj se učitava...

FOI Nastava

apps

mdi-login

Napredne formalne metode

Advanced Formal Methods
2015/2016

5 ECTSa

Informacijski i poslovni sustavi 1.1 (PDS)

Katedra za teorijske i primijenjene osnove informacijskih znanosti

6. 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	6	izborni

Cilj kolegija

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.).

Preduvjeti

Uvod u formalne metode (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
Čubrilo Mirko	Nositelj	Predavanja	15	2	1
Schatten Markus	Suradnik	Vježbe u praktikumu	15	1	1
Lovrenčić Sandra	Izvođač	Seminar	15	1	1

Sadržaj predavanja

Osnovni pojmovi, pregled sadržaja kolegija i literatura
Motivacija potrebe za kolegijem (konceptualno i logičko modeliranje sustava), programski jezici, alati i primjene. Razvoj ideje “simbolička logika kao programski jezik”.
Sintaksa računa predikata prvog reda
Abeceda računa predikata prvog reda (skupovi varijabli, konstanti, funkcijskih i predikatnih znakova, logičkih veznika, kvantifikatora i zagrada). Definicija terma. Definicija atomarne formule. Definicija formule. Reducirani zapis formule (pravila izostavljanja zagrada). Pojmovi slobodnog nastupa varijable u formuli i slobodne varijable. Pojam vezane varijable.
Prevođenje rečenica govornog jezika u jezik računa predikata
Podrijetlo funkcijskih i predikatnih znakova u jeziku računa predikata prvog reda. Sustavno prevođenje rečenica govornog jezika u jezik računa predikata prvog reda (problemi kontrole dosega kvantifikatora i upotrebe zagrada).
Osnove semantike računa predikata prvog reda
Pojam domene interpretacije. Definicija interpretacije terma. Definicija interpretacije atomarne formule. Definicija interpretacije formule. Pojam logiče posljedice za formule računa predikata. Ispunjive, identički istinite i kontradiktorne formule.
Primitivne normalne forme formula računa predikata prvog reda
Pojmovi konjunkta i disjunkta. Definicija primitivnih normalnih formi formula računa predikata prvog reda (prefiks i matrica). Popis transformacijskih tautologija za potrebe pretvaranja formula računa predikata prvog reda u primitivne normalne forme. Ekvivalentnost polazne forme i pripadajućih primitivnih normalnih formi.
Standardna ili Skolemova forma formula računa predikata prvog reda
Potreba za uklanjanjem egzistencijalnih kvantifikatora iz prefiksa primitivne normalne forme formule. Pravila uklanjanja egzistencijalnih kvantifikatora. Neekvivalentnost (u općem slučaju) polazne formule i njezine standardne forme. Ekvikontradiktornost polazne formule i njezine standardne formule.
Problemi proširenja pravila rezolucije s računa sudova na račun predikata
Motivirajući primjeri. Potreba za unifikacijom (ujednačavanjem) argumenata atomarnih formula. Pojam valuacije. Kompozicija valuacija
Algoritam unifikacije
Definicija unifikatora i maksimalnog unifikatora dvaju disjunkta. Algoritam unifikacije. Primjeri.
Pravilo rezolucije za račun predikata prvog reda
Definicija redukta dvaju disjunkta. Definicija binarne rezolvente dvaju disjunkta. Opća definicija rezolvente dvaju disjunkta. Primjeri.
Račun predikata prvog reda kao sredstvo za modeliranje i rješavanje problema
Pravilo rezolucije kao jezgra deduktivnog mehanizma. Opća shema primjene pravila rezolucije za račun predikata prvog reda u modeliranju i rješavanju problema. Problem ekstrakcije odgovora iz rezolucijskog izvoda identički lažnog ili kontradiktornog disjunkta. Uvođenje pomoćnog predikata %22Odgovor%22 i potpunost pravila rezolucije kao sredstva ekstrakcije odgovora. Modeliranje i rješavanje problema majmuna i banane. Modeliranje i rješavanje problema vuka, koze i kupusa.
Uvod u F-logiku
Potreba za spajanjem paradigmi objektno-orijentiranog i logičkog programiranja. F-logika kao teorijski okvir. Osnovni konstrukti F-logike.
Primjene F-logike
Nedostaje
Uvod u jezik OCL
Potreba za formalnom specifikacijom statičkih i dinamičkih aspekata UML dijagrama. OCL kao jezik specifikacije ograničenja (atributa, klasa, objekata, procesa). Referentne točke korištenja OCL-a u modeliranju UML dijagrama (jezik upita, specifikacija invarijanata klasa i tipova, specifikacija invarijanata za stereotipe, specifikacija preduvjeta i postuvjeta operacija nad klasama i metoda klasa,…).
Osnovni i korisnički tipovi podataka i konstrukta jezika OCL
Osnovni ugrađeni tipovi podataka jezika OCL. Osnovne operacije nad ugrađenim tipovima podataka. Naslijeđeni tipovi podataka iz jezika UML. Korisnički tipovi podataka. Programski konstrukti jezika OCL. Objekti i svojstva jezika OCL (u kontekstu integracije s jezikom UML).
Primjene jezika UML u specifikaciji UML dijagrama
Specifikacija „manjeg“ UML dijagrama iz domene poslovanja i ilusracija primjene jezika OCL.

Sadržaj seminara/vježbi

1. Tarski's World (uvod)
Tarski's World , Boole i Fitch – alati za učenje logike prvog reda (FOL). Uvod u alat Tarski's World. Sučelje i korišteni predikatni simboli. Kreiranje atomarnih rečenica – primjeri. Izgradnja vlastitog svijeta u Tarski's World. Pretvaranje jednostavnih rečenica iz prirodnog jezika u FOL – primjeri i zadaci. Dokazivanje – dedukcija i F sustav. Jednostavna pravila izvoda – eliminacija identitete, uvođenje identitete i reiteracija. Jednostavni primjeri dokazivanja.
2. Tarski's World (složene rečenice)
Kreiranje složenih rečenica u Tarski's World. Određivanje istinitosti rečenica koje koriste negaciju, konjunkciju i disjunkciju – primjeri i zadaci. Korištenje zagrada. Igradnja istinitog/lažnog svijeta prema zadanim rečenicama – zadaci. Pretvaranje rečenica u negacijsku normalnu formu – primjeri i zadaci.
3. Tarski's World (prevođenje rečenica) i Boole (tablice istinitosti)
Pravila dobrog prevođenja rečenica iz prirodnog jezika u FOL. Prevođenje složenih rečenica u Tarski's World i provjera prijevoda na zadanim svjetovima - zadaci. Uvod u alat za kreiranje tablica istinitosti Boole. Sučelje. Kreiranje tablice istinitosti i provjera. Provjera logičke posljedice pomoću tablice istinitosti. Primjeri i zadaci.
4. Fitch (kreiranje dokaza)
Fitch stil zapisa dokaza – F sustav. Uvod u alat za kreiranje dokaza Fitch. Sučelje. Pravila za uvođenje i eliminaciju konjunkcije, disjunkcije, negacije i kontradikcije. Korištenje poddokaza. Primjeri i zadaci.
5. Tarski's World (prevođenje rečenica)
Određivanje istinitosti rečenica koje koriste kondicional i bikondicional - primjeri. Prevođenje rečenica koje koriste kondicional i bikondicional u Tarski's World i provjera prijevoda na zadanim svjetovima - zadaci.
6. Fitch (kreiranje dokaza) i Tarski's World (varijable i kvantifikatori)
Pravila za uvođenje i eliminaciju kondicionala i bikondicionala. Dokazi bez pretpostavki. Primjeri i zadaci. Određivanje istinitosti rečenica koje koriste varijable i kvantifikatore - primjeri. Prevođenje rečenica koje koriste varijable i kvantifikatore u Tarski's World i provjera prijevoda na zadanim svjetovima - zadaci. Aristotelove forme – osnova prevođenja rečenica u FOL.
7. Fitch (kreiranje dokaza) i Tarski's World (višestruki kvantifikatori)
Pravila za uvođenje i eliminaciju unoverzalnog i egzistencijalnog kvantifikatora - primjeri i zadaci. Rečenice sa više kvantifikatora. Prevođenje rečenica koje koriste više kvantifikatora u Tarski's World i provjera prijevoda na zadanim svjetovima zadaci. Izvođenje dokaza na zadanim rečenicama - zadaci.
8. Fitch i Tarski's World (ponavljanje)
Samostalno rješavanje složenijih zadataka prevođenja i verificiranja rečenica, kao i izgradnje svjetova u Tarski's World. Samostalno kreiranje složenijih dokaza u Fitchu.

Ishodi učenja kolegija

razumjeti i primijeniti ključne aspekte informacijske tehnologije (programiranje, algoritmi, strukture podataka, baze podataka i znanja)
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 potrebu sustavnog i egzaktnog pristupa modeliranju i implementaciji informacijskih i poslovnih sustava te spoznati ulogu naprednih formalnih metoda (metoda simboličke logike) u tim procesima.
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.
Chang, C.; Lee, R.C. Symbolic logic and mechanical theorem proving. Academic Press, San Diego, 1973.
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.
Warmer, J.; Kleppe, A. The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley, Boston, 2003.
Clark, T.; Warmer, J. Object modeling with the OCL: the rationale behind the Object Constraint Language. Springer, Berlin, 2002.
Yang, G.; Kifer, M.; Zhao, C. Flora-2: User's Manual. Stony Brook, 2008. http://flora.sourceforge.net/docs/floraManual.pdf

Slični kolegiji

Prema dostupnim podacima, ekvivalentnih predmeta na dodiplomskim studijima u Republici Hrvatskoj nema. Postoje donekle srodni (po tematici i sadržaju) predmeti tipa “Logičko programiranje” (Filozofski fakultet-Zagreb), “Matematička logika” (filozofski fak

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.