Original title: Metoda sémantických stromů v neklasických logikách
Translated title: Tableaux in non-classical logics
Authors: Dančák, Michal ; Peliš, Michal (referee) ; Bílková, Marta (advisor)
Document type: Bachelor's theses
Year: 2009
Language: cze
Abstract: Dalo by se ríct, že jako dukazová metoda jsou sémantické stromy v Cesku nepríliš používané, a to i presto, že ve svete je to nejoblíbenejší dukazový systém pro modální logiku [1]. Vedle základního Hilbertova kalkulu se v ceské literature nejcasteji objevují sekventové kalkuly, prípadne kalkul prirozené dedukce. Presto má metoda sémantických stromu nekolik nezanedbatelných predností a zajímavých témat. Jak už název napovídá, tento kalkul vychází ze sémantiky - dukazy mají predevším sémantický charakter a pro "jednodušší" logiky jsou i velmi intuitivní. Dokazování je zároven i vyvracení. Pri dokazování metodou sémantických stromu vlastne hledáme protipríklad. Jestliže ho nenajdeme, a pokud jsme postupovali správne, tak neexistuje. Na poradí použití pravidel také nezáleží (až na nekolik vyjímek v nekterých logikách, které si pozdeji ukážeme). I díky temto výhodám je tato metoda také velmi vhodná pro strojové zpracování. V této práci jsem se rozhodl zamerit na to, jak se metoda sémantických stromu chová v substrukturální logice BCK (nekdy též FLew). Zacneme základními definicemi a tím, co to vlastne sémantické stromy jsou, dále bude následovat nekolik príkladu, definice logiky BCK a príslušných odvozovacích pravidel. Celá práce bude završena dukazem úplnosti a korektnosti tohoto kalkulu vuci kripkovské...

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/27214

Permalink: http://www.nusl.cz/ntk/nusl-282407


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Bachelor's theses