Please use this identifier to cite or link to this item: https://hdl.handle.net/10593/1016
Title: Logiki podstrukturalne oparte na dystrybutywnych kratach z rezyduacjami
Other Titles: Substructural logics based on distributed residuated lattices
Authors: Kozak, Michał
Advisor: Świrydowicz, Kazimierz. Promotor
Keywords: pełne rachunki Lambeka
full Lambek calculi
dystrybutywne kraty z rezyduacjami
distributed residuated lattices
kraty akcji
action lattices
rozstrzygalność
decidability
własność skończonego modelu
finite model property
Issue Date: 11-May-2011
Abstract: Praca traktuje o logikach podstrukturalnych, które są oparte na dystrybutywnych kratach z rezyduacjami. W pierwszej kolejności autor skupia się na podstawowym rachunku logicznym, którego modelem algebraicznym jest klasa dystrybutywnych krat z rezyduacjami, tzn. dystrybutywnym pełnym rachunku Lambeka. Dla rachunku tego, autor dowodzi własności skończonego modelu, a stąd rozstrzygalności tego rachunku. Oba te problemy były problemami długo otwartymi w literaturze. W dowodzie tym autor rozszerzył, szeroko stosowaną w systemach niedystrybutywnych, metodę nuklearnego domknięcia monoidu i quasi-zanurzenia na systemy dystrybutywne. Następnie autor wprowadza system dystrybutywnego pełnego rachunku Lambeka z cykliczną inwolucją i także dowodzi jego rozstrzygalności. Ponadto dla wersji niedystrybutywnej podaje pierwszy rozstrzygalny system z sekwentami intuicjonistycznymi. Na końcu, autor skupia się na infinitystycznych logikach akcji (tzn. logikach których modelami algebraicznymi są *-ciągłe kraty akcji) oraz rozszerza metodę nuklearnego domknięcia monoidu i quasi-zanurzenia zarówno na wersję dystrybutywną jak i niedystrybutywną. Dla wersji niedystrybutywnej ponadto dowodzi własności skończonego modelu.
The dissertation treats about substructural logics which are based on distributed residuated lattices. First, the author focuses on the basic logical calculus that algebraic model is the class of distributed residuated lattices, i.e. distributive full Lambek calculus. For this calculus, the author proves the finite model property, where from the decidability of this calculus follows. Both these problems were long-open problems in the literature. In this proof, the author extended the method of nuclei and quasi-embedding to distributive systems – so far, this method was known and widely used only for nondistributive systems. Next, the author introduces the system of cyclic involutive distributive full Lambek calculus and he proves its decidability as well. Moreover, for the nondistributive version, he gives the first decidable system with intuitionistic sequents. At the end, the author focuses on infinitary action logics (i.e. logics that algebraic models are *-continuous action lattices) and he extends the method of nuclei and quasi-embedding both to the distributive and to the nondistributive versions. In addition, for the nondistributive version, he proves the finite model property.
Description: Wydział Matematyki i Informatyki: Zakład Logiki Matematycznej
URI: http://hdl.handle.net/10593/1016
Appears in Collections:Doktoraty (WMiI)
Doktoraty 2010-2022 /dostęp ograniczony, możliwy z komputerów w Bibliotece Uniwersyteckiej/

Files in This Item:
File Description SizeFormat 
PhDmk.pdf
  Restricted Access
576.91 kBAdobe PDFView/Open
Show full item record



Items in AMUR are protected by copyright, with all rights reserved, unless otherwise indicated.