Logiki podstrukturalne oparte na dystrybutywnych kratach z rezyduacjami
Loading...
Date
2011-05-11T06:34:30Z
Authors
Advisor
Editor
Journal Title
Journal ISSN
Volume Title
Publisher
Title alternative
Substructural logics based on distributed residuated lattices
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.
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
Sponsor
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