Národní úložiště šedé literatury Nalezeno 10 záznamů.  Hledání trvalo 0.00 vteřin. 
Explicitní pevné body v logice dokazatelnosti
Chvalovský, Karel ; Švejdar, Vítězslav (vedoucí práce) ; Bílková, Marta (oponent)
Smyslem této diplomové práce je prozkoumat explicitní výpoty pevn ých bod v logice dokazatelnosti GL. Vta o pevných bodech zní: Pro kadou modální formuli A(p) v ní kadý výskyt atomu p je vázán modálním operátorem ¤, existuje formule D obsahující pouze výrokové atomy obsaené v A(p), neobsahující výrokový atom p, a taková, e v GL je dokazatelné D ' A(D). Formule D je navíc ur- ena a na dokazatelnou ekvivalenci jednoznan. Nejprve vyslovíme nkolik speciálních pípad vty o pevných bodech a poté podrobnji prozkoumáme vtu v plném znní. Dále ukáeme jednu sémantickou a dv syntaktické konstrukce pevných bod a dokáeme jejich korektnost. V práci se zabýváme také nkterými sloitostními aspekty konstrukce, pedevím uvádíme jednoduché horní odhady délky a modální sloitosti získaných pevných bod.
Důkazy pomocí konečných automatů
Fišer, Jan ; Holub, Štěpán (vedoucí práce) ; Chvalovský, Karel (oponent)
V roce 2016 zveřejnil Hamoon Mousavi program Walnut implementující automatické dokazování vět o automatických posloupnostech. Hlavním cílem této práce bylo ukázat teoretickou funkčnost Walnutu na základě spojitosti automatických posloupností s Presburgerovou (resp. Büchiho) aritmetikou, jež je rozhodnutelnou teorií. Dalším cílem bylo s přiměřenou mírou detailnosti popsat, jak je rozhodovací procedura Walnutem doopravdy prováděna, a na závěr pak na praktických příkladech ukázat možné využití Walnutu při řešení konrétních problémů. Jedním z těchto konkrétních příkladů, jejichž řešení je v práci předvedeno, je například nalezení kritického exponentu Rudin- Shapirovy posloupnosti - tento příklad je v literatuře z roku 2003 uváděn jako otevřený problém (nicméně v současnosti se již o otevřený problém nejedná, nebot' v roce 2011 Shallit dokázal, že kritický exponent všech auto- matických posloupností je vyčíslitelný). Samotnou poslední kapitolu lze také díky tomu, že obsahuje podrobně okomentované řešené příklady, využít jako velice stručný manuál pro ty, kteří se s Walnutem setkávají poprvé a chtějí jej využít k vlastním aplikacím. 1
Undecidability of Some Substructural Logics
Chvalovský, Karel ; Bílková, Marta (vedoucí práce) ; Buszkowski, Vojciech (oponent) ; Galatos, Nick (oponent)
Tato disertační práce se zabývá algoritmickou nerozhodnutelností (neřešitel- ností) dokazatelnosti v některých neklasických logikách. Ve skutečnosti existují dvě přirozené varianty toho problému. Mějme dánu logiku, pak můžeme studovat její množinu teorémů nebo její relaci důsledku, což je obecnější problém. Je známo, že oba tyto problémy mohou být nerozhod- nutelné již pro výrokové logiky a tato disertační práce poskytuje další pří- klady takových logik. Konkrétně se věnujeme výrokovým substrukturálním logikám, které lze získat ze sekventového kalkulu LJ pro intuicionistickou logiku odebráním strukturálních pravidel. Naše hlavní výsledky jsou násle- dující. Ukazujeme nerozhodnutelnost (konečné) relace důsledku pro některé základní neasociativní substrukturální logiky. Dále dokazujeme, že množina teorémů v základní substrukturální logice s pravidlem kontrakce, které ob- vykle způsobuje řadu komplikací, je nerozhodnutelná. Neboť studované logiky mají přirozené algebraické sémantiky, dostáváme také odpovídající algebraické výsledky, které jsou zajímavé samy o sobě.
Implikační fragmenty intuicionistické výrokové logiky
Blicha, Martin ; Švejdar, Vítězslav (vedoucí práce) ; Chvalovský, Karel (oponent)
V predloženej práci študujeme implikačné fragmenty intuicionistickej výrokovej logiky s konečným počtom atómov. V prvej časti sa podrobnejšie venujeme fragmentu s dvomi atómami, ktorý je dostatočne jednoduchý, aby v ňom bolo možné sledovať vzťahy medzi formulami, zároveň ale nie je príliš triviálny. V ďalšej časti zavádzame pojmy principálny vrchol a principálny model, ktoré nám umožnia skúmať aj ďalšie fragmenty. V poslednej časti zisťujeme, ako sa zmenia výsledky, ak si do jazyka pridáme konštantu .
Explicitní pevné body v logice dokazatelnosti
Chvalovský, Karel ; Bílková, Marta (oponent) ; Švejdar, Vítězslav (vedoucí práce)
Smyslem této diplomové práce je prozkoumat explicitní výpoty pevn ých bod v logice dokazatelnosti GL. Vta o pevných bodech zní: Pro kadou modální formuli A(p) v ní kadý výskyt atomu p je vázán modálním operátorem ¤, existuje formule D obsahující pouze výrokové atomy obsaené v A(p), neobsahující výrokový atom p, a taková, e v GL je dokazatelné D ' A(D). Formule D je navíc ur- ena a na dokazatelnou ekvivalenci jednoznan. Nejprve vyslovíme nkolik speciálních pípad vty o pevných bodech a poté podrobnji prozkoumáme vtu v plném znní. Dále ukáeme jednu sémantickou a dv syntaktické konstrukce pevných bod a dokáeme jejich korektnost. V práci se zabýváme také nkterými sloitostními aspekty konstrukce, pedevím uvádíme jednoduché horní odhady délky a modální sloitosti získaných pevných bod.
Notes on Condensed Detachment
Chvalovský, Karel
Plný tet: 0364974 - Stáhnout plný textPDF
Plný text: content.csg - Stáhnout plný textPDF
Logic, Algebra and Truth Degrees 2010
Chvalovský, Karel ; Cintula, Petr ; Noguera, C.
Volume of abstracts from the conference Logic, Algebra and Truth Degrees 2010 (the second official meeting of the EUSFLAT Working Group on Mathematical Fuzzy Logic) which was held on 7-11 September 2010 in Prague. The volume was published by Institute of Theoretical informatics as volume 2010-502 of ITI Series and is available at http://iti.mff.cuni.cz/series/
Syntactic Approach to Fuzzy Modal Logic in MTL
Chvalovský, Karel
Plný tet: 0328861 - Stáhnout plný textPDF
Plný text: content.csg - Stáhnout plný textPDF
On the Independence of Axioms in BL and MTL
Chvalovský, Karel
Plný tet: 0312146 - Stáhnout plný textPDF
Plný text: content.csg - Stáhnout plný textPDF

Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.