Formalizace relace odvoditelnosti pro výrokové fuzzy logiky

• Thesis title in Czech: Formalizace relace odvoditelnosti pro výrokové fuzzy logiky
• Thesis title in English: Formalization of the deducibility relation of propositional fuzzy logics
• Key words: Basic logic, Isabelle, HOL, automatické dokazování, formalizace
• English key words: Basic logic, Isabelle, HOL, automated proving, formalization
• Academic year of topic announcement: 2012/2013
• Thesis type: Bachelor's thesis
• Thesis language: čeština
• Department: Department of Logic (21-KLOG)
• Supervisor: Mgr. Libor Běhounek, Ph.D.
• Author: hidden - assigned and confirmed by the Study Dept.
• Date of registration: 01.02.2013
• Date of assignment: 01.02.2013
• Administrator's approval: not processed yet
• Confirmed by Study dept. on: 12.02.2013
• Date and time of defence: 01.02.2016 09:00
• Date of electronic submission: 19.08.2014
• Date of proceeded defence: 01.02.2016
• Submitted/finalized: committed by student and finalized
• Opponents: Mgr. Josef Urban, Ph.D.

Guidelines

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.

References

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.