Home > Search Results: Révay, Petr
Search:
Search Tips :: Advanced Search
Search collections:
Sort by: Display results: Output format:
National Repository of Grey Literature 2 records found  Search took 0.01 seconds. 
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 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)
Detailed record
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 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)
Detailed record

Interested in being notified about new results for this query?
Subscribe to the RSS feed.
Digital Repository :: Search :: Submit :: Personalize :: Help
Powered by Invenio v1.1.2
Maintained by admin.invenio@techlib.cz
This site is also available in the following languages:
Česky  English