
Formalization of the deducibility relation of propositional fuzzy logics
Révay, Petr ; Běhounek, Libor (advisor) ; Urban, Josef (referee)
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 computerverified proofs of some theorems and syntactic metatheorems 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 proofchecker 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)


Formalization of the deducibility relation of propositional fuzzy logics
Révay, Petr ; Běhounek, Libor (advisor) ; Urban, Josef (referee)
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 computerverified proofs of some theorems and syntactic metatheorems 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 proofchecker 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)


Systémy morfismů nad Gödelovou fuzzy logikou
Luhan, Ondřej ; Běhounek, Libor (advisor) ; Haniková, Zuzana (referee)
This work introduces some very basic concepts of category theory as built up over firstorder predicate Gödel fuzzy logic (with crisp identity and the delta operator). A fuzzy variation of a classical concept of a category is considered. Then several systems of morphisms loosely based on the crisp categories Rel and Set are defined and examined. Accordingly, all the systems under consideration consist of fuzzy sets as objects and various kinds of binary fuzzy relations as morphisms. Our approach is a logicbased graded generalization of crisp (clas sical) categorytheoretical approaches to fuzzy sets, which have been initiated by Goguen. 1


Algebraic and Kripke semantics of substructural logics
Arazim, Pavel ; Bílková, Marta (advisor) ; Běhounek, Libor (referee)
This thesis is about the distributive full Lambek calculus, i.e., intuicionistic logic without the structural rules of exchange, contraction and weakening and particularly about the two semantics of this logic, one of which is algebraic, the other one is a Kripke semantic. The two semantics are treated in separate chapters and some results about them are shown, for example the disjunction property is proven by amalgamation of Kripke models. The core of this thesis is nevertheless the relation of these two semantics, since it is interesting to study what do they have in common and how can they actually differ, both being a semantics of the same logic. We show how to translate frames to algebras and algebras to frames, and, moreover, we extend such translation to morphisms, thus constructing two functors between the two categories. Key words:distributive FL logic, distributive full Lambek calculus, structural rules, distributive residuated lattice, Kripke frames, frame morphisms, category, functor 2

 

Categories of fuzzy sets
Luhan, Ondřej ; Bílková, Marta (referee) ; Běhounek, Libor (advisor)
Category theory provides very useful tools for studying mathematical structures and phenomena. One of the structures that is studied in a categorytheoretical manner are fuzzy sets. If we consider fuzzy sets as objects and set up certain kind of structure preserving mappings as morphisms, we can obtain a suitable category for our purposes. Goal of this work is to give an overview of preferably all important categorytheoretical approaches to fuzzy sets that were done throughout relatively short history of categorytheoretical modelling of fuzzy sets.


Logical foundations of fuzzy mathematics
Běhounek, Libor ; Jirků, Petr (advisor) ; Gottwald, Siegfried Johannes (referee) ; Dvořák, Antonín (referee)
The dissertation consists of the author's published papers on logicbased fuzzy mathe matics. It is accompanied with a cover study (Part I of the thesis), which introduces the area of logicbased fuzzy mathematics, argues for the signicance of the area of re search, presents the state of the art, indicates the author's contribution to the eld, and comments on the papers comprising the thesis. Fuzzy mathematics can be characterized as the study of fuzzy structures, i.e., math ematical structures in which the two values 0, 1 are at some points replaced by a richer system of degrees. Under the logicbased approach, fuzzy structures are formalized by means of axiomatic theories over suitable systems of fuzzy logic, whose rules replace the rules of classical logic in formal derivation of theorems. The main advantages of the logicbased approach are the general gradedness of dened notions, methodological clarity provided by the axiomatic method, and the applicability of a foundational architecture mimicking that of classical mathematics. Logicbased fuzzy mathematics is part of a broader area of nonclassical mathematics (i.e., mathematical disciplines axiomatizable in nonclassical logics), as well as a specic subeld of general fuzzy methods. Following earlier isolated developments in logicbased fuzzy set...


Fuzzification of simple systems of deontic logic
Vostrá, Nelly ; Bílková, Marta (referee) ; Běhounek, Libor (advisor)
Deontické logiky bývají formalizovány jako druh modálních logik. V této práci aplikuji fuzzy modální logiku na dvojí systémy monadick ých deontických logik  systémy deontické logiky v užším smyslu a systémy alethické logiky s výrokovou konstantou Q. Pro tyto nové fuzzy deontické logiky dokazuji lokální větu o dedukci, korektnost vřuči příslušným fuzzy rámcřum a definovatelnost deontick ých systémřu v alethických.

 
 