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
Napredne formalne metode
Advanced Formal Methods
2017/2018
5 ECTSa
Informacijski i poslovni sustavi 1.1 (PDS)
Katedra za teorijske i primijenjene osnove informacijskih znanosti
RI
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 0 0 0
Schatten Markus Suradnik Vježbe u praktikumu 0 0 0
Lovrenčić Sandra Izvođač Seminar 0 0 0
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.
 2024 © Fakultet organizacije i informatike, Centar za razvoj programskih proizvoda