Formalizace relace odvoditelnosti pro výrokové fuzzy logiky

Abstract

Tato 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)