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.