|
|
Formalizace relace odvoditelnosti pro výrokové fuzzy logiky
Révay, Petr ; Běhounek, Libor (vedoucí práce) ; Urban, Josef (oponent)
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)
|
|
|
Formalizace relace odvoditelnosti pro výrokové fuzzy logiky
Révay, Petr ; Běhounek, Libor (vedoucí práce) ; Urban, Josef (oponent)
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)
|
|
|
Systémy morfismů nad Gödelovou fuzzy logikou
Luhan, Ondřej ; Běhounek, Libor (vedoucí práce) ; Haniková, Zuzana (oponent)
V práci jsou zavedeny některé velice základní pojmy teorie kategorií budované nad prvořádovou Gödelovou fuzzy logikou (s ostrou rovností a delta operá- torem). Fuzzy varianta klasického pojmu kategorie je uvážena. Následně je defi- nováno a prozkoumáno několik systémů morfismů volně vycházejících z ostrých kategorií Rel a Set. Všechny uvažované systémy tudíž obsahují fuzzy množiny jako objekty a různé druhy binárních fuzzy relací jako morfismy. Náš přístup je logicky-založené stupňované zobecnění ostrých (klasických) kategoriálně-teore- tických přístupů k fuzzy množinám, které byly iniciovány Goguenem. 1
|
|
|
Algebraic and Kripke semantics of substructural logics
Arazim, Pavel ; Bílková, Marta (vedoucí práce) ; Běhounek, Libor (oponent)
Tato práce se zabývá distributivním Lambekovým kalkulem, tedy intuicionistickou logikou bez pravidel záměny, kontrakce a oslabení, a především dvěma různými sé- mantikami této logiky, totiž sémantikou algebraickou a kripkovskou. Tyto dvě séman- tiky jsou nejdříve pojednávány ve zvláštních kapitolách a jsou prezentovány některé výsledky, které se jich týkají, např. se ukáže vlastnostnost disjunkce pomocí sloučení dvou Kripkovských modelů. Jádrem práce je nicméně především vztah těchto dvou sémantik, protože je zajímavé porovnávat, co mají společného, a čím se vůbec mohou lišit, když jsou obě sémantikami téže logiky. Bude ukázán překlad kripkovských rámců na algebry a algeber na rámce a dále bude tento překlad rožšířen i na morfismy, čímž budou zkonstruovány dva funktory mezi oběma kategoriemi. Klíčová slova:distributivní logika FL, distributivní Lambekův kalkul, strukturální pravidla, distributivní residuované svazy, kripkovské rámce, morfismy mezi rámci, kategorie, funktor 3
|
|
| |
|
|
Categories of fuzzy sets
Luhan, Ondřej ; Bílková, Marta (oponent) ; Běhounek, Libor (vedoucí práce)
Category theory provides very useful tools for studying mathematical structures and phenomena. One of the structures that is studied in a category-theoretical 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 category-theoretical approaches to fuzzy sets that were done throughout relatively short history of category-theoretical modelling of fuzzy sets.
|
|
|
Logical foundations of fuzzy mathematics
Běhounek, Libor ; Jirků, Petr (vedoucí práce) ; Gottwald, Siegfried Johannes (oponent) ; Dvořák, Antonín (oponent)
Předložená disertační práce sestává z autorových publikovaných článků o logických základech fuzzy matematiky, doplněných strhující studií (tvoricich úvodní část disertace), ve které je představen formálně logický přístup k fuzzy matematice. Dále je v ní dokládána důležitost výzkumu v tomto oboru a charakterizován jeho současný stav, popsán autorův příspěvek k oboru a podány komentare k jednotlivým článkům, z nichž disertace skládá.
|
|
|
Fuzzifikace jednoduchých systémů deontické logiky
Vostrá, Nelly ; Bílková, Marta (oponent) ; Běhounek, Libor (vedoucí práce)
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.
|
|
| |
|
| |
host ::
RSS.