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