FOI nastava
FOI logo

Lista kolegija iz:

ak.god:
2018/2019
semestar:
6. semestar

2018/2019

5ECTSa

Preddiplomski

Informacijski/Poslovni sustavi v1.1

Program Obavezan
Informacijski sustavi IS Ne
Poslovni sustavi PS Ne
6. semestar
3. nastavna godina

Napredne formalne metode npp:72635

Engleski naziv

Advanced Formal Methods

Katedra

Katedra za teorijske i primijenjene osnove informacijskih znanosti

Kategorija ("boja")

RI

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

Nastava

Predavanje
30sati
Seminar
15sati
Laboratorijske vježbe
15sati

Ishodi učenja predmeta

  • 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
  • konceptualno i formalno modelirati različite segmente informacijskih i poslovnih sustava
  • razumjeti i primijeniti ključne aspekte informacijske tehnologije (programiranje, algoritmi, strukture podataka, baze podataka i znanja)
  • 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.

Ishodi učenja programa

  • modelirati poslovne procese i podatke u organizacijama i primijeniti modele u razvoju informacijskih i poslovnih sustavamodelirati poslovne procese i podatke u organizacijama i primijeniti modele u razvoju informacijskih i poslovnih sustava
  • 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 temepratiti 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 matematičke metode, modele i tehnike primjerene rješavanju problema iz područja informacijskih i poslovnih sustava razumjeti i primijeniti matematičke metode, modele i tehnike primjerene rješavanju problema iz područja informacijskih i poslovnih sustava

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.

Alati koji se koriste na predmetu

  • Tarski's World
    Alat za učenje logike prvog reda. Dolazi sa knjigom - Barwise, Jon; Etchemendy, John: Language, proof and logic, CSLI Publications, Stanford, 1999.
  • Boole
    Alat za učenje kreiranja tablica istinitosti i njihovog korištenja. Dolazi sa knjigom - Barwise, Jon; Etchemendy, John: Language, proof and logic, CSLI Publications, Stanford, 1999.
  • Fitch
    Alat za učenje kreiranja dokaza dedukcijom. Dolazi sa knjigom - Barwise, Jon; Etchemendy, John: Language, proof and logic, CSLI Publications, Stanford, 1999.

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

Preduvjeti

  • Uvod u formalne metode
    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.

Slični predmeti

  • 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
Nastavnik Oblik nastave Tjedana Sati tjedno Grupa
Schatten Markus Laboratorijske vježbe 0 0 0
Predavanje 0 0 0
Seminar 0 0 0
Nema definiranih ispitnih rokova

Napredne formalne metode - Redovni studenti

Studij: Informacijski/Poslovni sustavi
Akademska godina: 2018/2019

Praćenje rada studenata

Elementi praćenjaBodova
Prisustvovanje nastavi5
Aktivnost na nastavi5
Seminar 30
Kolokviji60
ZBROJ100


Bodovna skala ocjena

OdDoOcjena
0 49 nedovoljan (1)
50 60 dovoljan (2)
61 75 dobar (3)
76 90 vrlo dobar (4)
91 100 odličan (5)



Kolokviji

Naziv / Tjedan 1234567891011121314151617 1. razdoblje
udio (%)
2. razdoblje
udio (%)
3. razdoblje
udio (%)
Trajanje Pismeni Usmeni
1. kolokvij + 100.0 90 +
2. kolokvij + 10.0 90.0 90 +


Opis elemenata praćenja

Elementi praćenja Bodovi Uvjet Opis Nadoknada
Granica Opis Rok
Prisustvovanje na seminarima 5 0 Uvjet za potpis. Na seminarima se 5 puta nasumično obavlja provjera prisustvovanja. Dozvoljena su 3 izostanka. Student dobiva onoliko bodova koliko je puta bio prisutan u vrijeme provjere. 5 izostanaka Dodatni referat. Javiti se nastavniku nakon objave evidencije prisustvovanja, najkasnije do kraja 15. tjedna. Zadnji dan 17. tjedna.
Prisustvovanje na laboratorijskim vježbama 0 0 Uvjet za potpis. Na svim laboratorijskim vježbama provjerava se prisustvovanje. Dozvoljen je 1 izostanak (vježbe se provode kroz 8 tjedana po 2 sata). 2 izostanka Dodatni zadaci. Javiti se nastavniku nakon objave evidencije prisustvovanja, najkasnije do kraja 15. tjedna. Zadnji dan 17. tjedna.
Aktivnost na laboratorijskim vježbama i seminarima 5 0 Studenti mogu sudjelovati u diskusijama na laboratorijskim vježbama i seminarima, prezentirati rješenja pojedinih zadataka i sl., za što ukupno mogu dobiti 5 bodova.
Seminar 30 0 Nije obavezan. Student ili grupa (do 3 studenta u timu) dobiva temu seminara. Pismeni dio seminara treba postaviti na Web unutar zadanog roka te prezentirati seminar uz prezentaciju u nekom alatu u dogovorenom terminu. Korištenje tuđeg rješenja i plagiranje je zabranjeno te povlači disciplinsku odgovornost.
1. kolokvij* 30 20 Rješavanje zadataka uz dodatak teoretskih pitanja otvorenog tipa i pitanja koja ispituju razumijevanje. Prepisivanje je zabranjeno te povlači disciplinsku odgovornost.
Na oba kolokvija ukupno mora biti ostvareno najmanje 20 bodova.
2. kolokvij 30 Rješavanje zadataka uz dodatak teoretskih pitanja otvorenog tipa i pitanja koja ispituju razumijevanje. Prepisivanje je zabranjeno te povlači disciplinsku odgovornost.
Na oba kolokvija ukupno mora biti ostvareno najmanje 20 bodova.


*Na kolokvijima ukupno mora biti ostvareno najmanje 20 bodova kako bi student mogao predmet položiti tijekom godine kroz kontinuirano praćenje.

 

Napredne formalne metode - Izvanredni studenti

Studij: Informacijski/Poslovni sustavi
Akademska godina: 2018/2019

Studenti mogu položiti predmet na sljedeće načine:

  1. Redovni izlazak na pismeni i usmeni ispit - Model 1;
  2. Izrada i obrana opsežnijeg seminarskog rada na zadanu temu (nije moguće ako su laboratorijske vježbe odrađivane kod kuće) - Model 2;
  3. Sudjelovanje u kontinuiranom praćenju na isti način kao i redoviti studenti – Model 3;
  4. Sudjelovanje u kontinuiranom praćenju kroz e-učenje i samostalni rad - Model 4.

Praćenje rada studenata - Model 3

Elementi praćenjaBodova
Prisustvovanje nastavi5
Aktivnost na nastavi5
Seminar 30
Kolokviji60
ZBROJ100


Praćenje rada studenata - Model 4

Elementi praćenjaBodova
Primjer usporedbe metoda dokazivanja10
Seminar30
Kolokviji60
ZBROJ100


Bodovna skala ocjena

OdDoOcjena
0 49 nedovoljan (1)
50 60 dovoljan (2)
61 75 dobar (3)
76 90 vrlo dobar (4)
91 100 odličan (5)



Kolokviji

Naziv / Tjedan 1234567891011121314151617 1. razdoblje
udio (%)
2. razdoblje
udio (%)
3. razdoblje
udio (%)
Trajanje Pismeni Usmeni
1. kolokvij + 100.0 90 +
2. kolokvij + 10.0 90.0 90 +


Opis elemenata praćenja - Model 3

Elementi praćenja Bodovi Uvjet Opis Nadoknada
Granica Opis Rok
Prisustvovanje na seminarima 5 0 Na seminarima se 5 puta nasumično obavlja provjera prisustvovanja. Student dobiva onoliko bodova koliko je puta bio prisutan u vrijeme provjere.
Prisustvovanje na laboratorijskim vježbama 0 0 Uvjet za potpis. Na svim laboratorijskim vježbama provjerava se prisustvovanje. Dozvoljena su 2 izostanka (vježbe se provode kroz 8 tjedana po 2 sata). U posebnim slučajevima vježbe se mogu odraditi kod kuće 4 izostanka Dodatni zadaci. Javiti se nastavniku nakon objave evidencije prisustvovanja, najkasnije do kraja 15. tjedna. Zadnji dan 17. tjedna.
Aktivnost na laboratorijskim vježbama i seminarima 5 0 Studenti mogu sudjelovati u diskusijama na laboratorijskim vježbama i seminarima, prezentirati rješenja pojedinih zadataka i sl., za što ukupno mogu dobiti 5 bodova.
Seminar 30 0 Nije obavezan. Student ili grupa (do 3 studenta u timu) dobiva temu seminara. Pismeni dio seminara treba postaviti na Web unutar zadanog roka te prezentirati seminar uz prezentaciju u nekom alatu u dogovorenom terminu. Korištenje tuđeg rješenja (plagijat) je zabranjeno te povlači disciplinsku odgovornost.
1. kolokvij* 30 20 Rješavanje zadataka uz dodatak teoretskih pitanja otvorenog tipa i pitanja koja ispituju razumijevanje. Prepisivanje je zabranjeno te povlači disciplinsku odgovornost.
Na oba kolokvija ukupno mora biti ostvareno najmanje 20 bodova.
2. kolokvij 30 Rješavanje zadataka uz dodatak teoretskih pitanja otvorenog tipa i pitanja koja ispituju razumijevanje. Prepisivanje je zabranjeno te povlači disciplinsku odgovornost.
Na oba kolokvija ukupno mora biti ostvareno najmanje 20 bodova.


Opis elemenata praćenja - Model 4

Elementi praćenja Bodovi Uvjet Opis Nadoknada
Granica Opis Rok
Prisustvovanje na laboratorijskim vježbama 0 0 Uvjet za potpis. Na svim laboratorijskim vježbama provjerava se prisustvovanje. Dozvoljena su 2 izostanka (vježbe se provode kroz 8 tjedana po 2 sata). U posebnim slučajevima vježbe se mogu odraditi kod kuće 4 izostanka Dodatni zadaci. Javiti se nastavniku nakon objave evidencije prisustvovanja, najkasnije do kraja 15. tjedna. Zadnji dan 17. tjedna.
Primjer usporedbe metoda dokazivanja 10 0 Student dobiva zadatak usporedbe metoda dokazivanja koji treba predati u obliku kraćeg seminara i obrazložiti na konzultacijama.
Seminar 30 0 Nije obavezan. Student ili grupa (do 3 studenta u timu) dobiva temu seminara. Pismeni dio seminara treba postaviti na Web unutar zadanog roka te prezentirati seminar uz prezentaciju u nekom alatu u dogovorenom terminu. Korištenje tuđeg rješenja (plagijat) je zabranjeno te povlači disciplinsku odgovornost.
1. kolokvij* 30 20 Rješavanje zadataka uz dodatak teoretskih pitanja otvorenog tipa i pitanja koja ispituju razumijevanje. Prepisivanje je zabranjeno te povlači disciplinsku odgovornost. Na oba kolokvija ukupno mora biti ostvareno najmanje 20 bodova.
2. kolokvij 30 Rješavanje zadataka uz dodatak teoretskih pitanja otvorenog tipa i pitanja koja ispituju razumijevanje. Prepisivanje je zabranjeno te povlači disciplinsku odgovornost. Na oba kolokvija ukupno mora biti ostvareno najmanje 20 bodova.


*Na kolokvijima ukupno mora biti ostvareno najmanje 20 bodova kako bi student mogao predmet položiti tijekom godine kroz kontinuirano praćenje.

 

Nema podataka o rasporedu
Copyright © 2015 FOI Varaždin. All Rights Reserved. Sva prava pridržana.
Povratak na vrh