Formalizace relace odvoditelnosti pro výrokové fuzzy logiky
Název práce v češtině: | Formalizace relace odvoditelnosti pro výrokové fuzzy logiky |
---|---|
Název v anglickém jazyce: | Formalization of the deducibility relation of propositional fuzzy logics |
Klíčová slova: | Basic logic, Isabelle, HOL, automatické dokazování, formalizace |
Klíčová slova anglicky: | Basic logic, Isabelle, HOL, automated proving, formalization |
Akademický rok vypsání: | 2012/2013 |
Typ práce: | bakalářská práce |
Jazyk práce: | čeština |
Ústav: | Katedra logiky (21-KLOG) |
Vedoucí / školitel: | Mgr. Libor Běhounek, Ph.D. |
Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
Datum přihlášení: | 01.02.2013 |
Datum zadání: | 01.02.2013 |
Schválení administrátorem: | zatím neschvalováno |
Datum potvrzení stud. oddělením: | 12.02.2013 |
Datum a čas obhajoby: | 01.02.2016 09:00 |
Datum odevzdání elektronické podoby: | 19.08.2014 |
Datum proběhlé obhajoby: | 01.02.2016 |
Odevzdaná/finalizovaná: | odevzdaná studentem a finalizovaná |
Oponenti: | Mgr. Josef Urban, Ph.D. |
Zásady pro vypracování |
V systému pro formalizaci matematiky Isabelle/Isar (či jeho vhodné nadstavbě, např. Isabelle/HOL) formalizujte základní syntaktické pojmy klasické metamatematiky (zejména pojmy formule, důkazu a odvoditelnosti v hilbertovském kalkulu) pro vybrané výrokové fuzzy logiky, zejména Goedelovu, Lukasiewiczovu, produktovou, BL a MTL. Formalizací důkazů popsaných v literatuře demonstrujte ve vybudovaném aparátu dokazatelnost základních výrokových teorémů příslušných logik. Zdrojové texty formalizace v systému Isabelle popište a dostatečně zdokumentujte tak, aby byly využitelné pro rozšíření směrem k formalizaci dalších partií metamatematiky fuzzy logiky.
V systému pro formalizaci matematiky Isabelle/Isar (či jeho vhodné nadstavbě, např. Isabelle/HOL) formalizujte základní syntaktické pojmy klasické metamatematiky (zejména pojmy formule, důkazu a odvoditelnosti v hilbertovském kalkulu) pro vybrané výrokové fuzzy logiky, zejména Goedelovu, Lukasiewiczovu, produktovou, BL a MTL. Formalizací důkazů popsaných v literatuře demonstrujte ve vybudovaném aparátu dokazatelnost základních výrokových teorémů příslušných logik. Zdrojové texty formalizace v systému Isabelle popište a dostatečně zdokumentujte tak, aby byly využitelné pro rozšíření směrem k formalizaci dalších partií metamatematiky fuzzy logiky. |
Seznam odborné literatury |
Běhounek L., Cintula P., Hájek P.: Introduction to mathematical fuzzy logic. In P. Cintula, P. Hájek, C. Noguera (eds.): Handbook of Mathematical Fuzzy Logic, pp. 1–101, College Publications, 2011. (Odd. 1–2.)
Hájek P.: Metamathematics of Fuzzy Logic. Kluwer 1998. (Kap. 1–4.) Sochor A.: Klasická matematická logika. Karolinum 2001. (Kap. 1.) Nipkow T.: Programming and Proving in Isabelle/HOL, http://isabelle.in.tum.de/dist/Isabelle2012/doc/prog-prove.pdf. Nipkow T., Paulson L. C., Wenzel M.: A Proof Assistant for Higher-Order Logic, http://isabelle.in.tum.de/dist/Isabelle2012/doc/tutorial.pdf. Instalace a dokumentace systému Isabelle, http://isabelle.in.tum.de. |