Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 4

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus

100%
Indrzejczak A.
Bulletin of the Section of Logic
|
2016
|
tom 45
|
nr 2
EN
In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi (SC) for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form.
2
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

Cut Elimination Theorem for Non-Commutative Hypersequent Calculus

100%
Indrzejczak A.
Bulletin of the Section of Logic
|
2017
|
tom 46
|
nr 1/2
EN
Hypersequent calculi (HC) can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.
3
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

Rule-Generation Theorem and its Applications

100%
Indrzejczak A.
Bulletin of the Section of Logic
|
2018
|
tom 47
|
nr 4
EN
In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some case studies for illustration.
4
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

Professor Grzegorz Malinowski in Honorem

63%
Indrzejczak A., Ciuciura J.
Bulletin of the Section of Logic
|
2017
|
tom 46
|
nr 1/2
EN
-
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.