Formalizace relace odvoditelnosti pro výrokové fuzzy logiky
Formalization of the deducibility relation of propositional fuzzy logics
bakalářská práce (OBHÁJENO)
![Náhled dokumentu](/bitstream/handle/20.500.11956/80580/thumbnail.png?sequence=8&isAllowed=y)
Zobrazit/ otevřít
Trvalý odkaz
http://hdl.handle.net/20.500.11956/80580Identifikátory
SIS: 133631
Kolekce
- Kvalifikační práce [23201]
Autor
Vedoucí práce
Oponent práce
Urban, Josef
Fakulta / součást
Filozofická fakulta
Obor
Logika
Katedra / ústav / klinika
Katedra logiky
Datum obhajoby
1. 2. 2016
Nakladatel
Univerzita Karlova, Filozofická fakultaJazyk
Čeština
Známka
Výborně
Klíčová slova (česky)
Basic logic, Isabelle, HOL, automatické dokazování, formalizaceKlíčová slova (anglicky)
Basic logic, Isabelle, HOL, automated proving, formalizationTato bakalářská práce předkládá formalizaci relace odvoditelnosti fuzzy logiky BL v prostředí matematického asistenta Isabelle/HOL a počítačově ověřené důkazy některých teorémů a meta-teorémů této logiky. Zároveň poskytuje popis procesu formalizace a použité prostředky Isabelle/HOL předvádí na jednodušších příkladech. Samostatná kapitola je pak věnována úvodu do logiky BL. Po nastudování dokumentace a volbě vhodných nástrojů Isabelle/HOL byla implementována formalizace, díky níž lze v programu ověřovat důkazy jak v axiomatizaci BL, tak i důkazy vlastností relace dokazatelnosti. Z těch byl formalizován především důkaz věty o lokální dedukci. Dále byly formalizovány důkazy řady teorémů BL, a to včetně odvození redundantních axiomů BL2 a BL3. Přínosem této práce je prozkoumání možností verifikátoru Isabelle/HOL z hlediska použití pro fuzzy logiku BL. Vzhledem k uvedeným poznatkům je možné práci použít jako základ širšího projektu formalizace fuzzy logik, které z logiky BL vycházejí. Powered by TCPDF (www.tcpdf.org)
This bachelor thesis presents the formalization of provability relation of fuzzy logic BL in the environment of a mathematical assistant Isabelle/HOL and also the computer-verified proofs of some theorems and syntactic meta-theorems of this logic. It also provides a description of the process of formalization and describes the tools of Isabelle/HOL used in the code by simple examples. The separate chapter is devoted to the introduction to the logic BL. The formalization has been implemented after studying the documentation and choosing of the appropriate methods of Isabelle/HOL. The formalization allows the software to verify the proofs in the axiomatization of BL, and moreover, of the properties of the provability relation itself. Especially, the proof of the local deduction theorem has been formalized as well as the proofs of the theorems of BL, including the derivations of the redundant axioms BL2 and BL3. The major objective of this bachelor thesis is to explore the possibilities of the proof-checker Isabelle/HOL in terms of fuzzy logic BL. With respect to the obtained results the thesis can be used as the starting point of a wider project of formalization of the others fuzzy logics which are based on the logic BL. Powered by TCPDF (www.tcpdf.org)