FOI nastava
FOI logo

Lista kolegija iz:

ak.god:
2013/2014
semestar:
3. semestar

2013/2014

5ECTSa

Preddiplomski

Informacijski/Poslovni sustavi v1.1

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

Uvod u formalne metode npp:61779

Engleski naziv

Introduction to Formal Methods

Katedra

Katedra za teorijske i primijenjene osnove informacijskih znanosti

Kategorija ("boja")

RI

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.

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
  • 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
  • ovladati idejnim postavkama i osnovnim tehnikama logičkog programiranja
  • raditi u timu za izgradnju informacijskih 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 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
  • razumjeti i primijeniti metode, tehnike razvoja informacijskih i programskih sustava u suvremenim razvojnim okolinama razumjeti i primijeniti metode, tehnike razvoja informacijskih i programskih sustava u suvremenim razvojnim okolinama

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.

Alati koji se koriste na predmetu

  • SWI-Prolog
    Besplatan alat za učenje osnova logičkog programiranja.
  • SWI-Prolog-Editor
    Besplatno sučelje za SWI-Prolog namijenjeno lakšem učenju Prologa.

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.

Preduvjeti

  • Matematika 1
    Cilj predmeta Matematika I je upoznavanje studenata s osnovnim pojmovima diskretne matematike (kao što su matematički modeli, matematička logika te skupovi i relacije) i linearne algebre (matrice, determinante, sustavi linearnih jednadžbi i nejednadžbi) koji su neophodni za prihvaćanje kvantitativnih aspekata znanja u informacijskim i organizacijskim znanostima te priprema studenata za logičko razmišljanje u znanosti i poslovanju. Predmet ima i generičke ciljeve kao što su timski rad, prezentacijske vještine (usmeno i pismeno izražavanje), razumijevanje modela, upotreba literature i razvoj ICT vještina, te posebno strategije rješavanja problemskih zadataka. Nadalje, koncepcija rada omogućava razvoj vještina apstrakcije kod studenata

Slični predmeti

  • 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),…
Nastavnik Oblik nastave Tjedana Sati tjedno Grupa
Čubrilo Mirko Predavanje 15 2 2
Lovrenčić Sandra Laboratorijske vježbe 15 1 9
Seminar 15 1 4
Nema definiranih ispitnih rokova
Predavanje Seminar Auditorne vježbe Laboratorijske vježbe Vježbe (jezici, tzk) Ispit Kolokviji Nadoknade Demonstrature
Copyright © 2015 FOI Varaždin. All Rights Reserved. Sva prava pridržana.
Povratak na vrh