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: 6

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

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych:  cut elimination
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

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.
2
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.
3
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity

88%
Buszkowski W.
Bulletin of the Section of Logic
|
2017
|
tom 46
|
nr 1/2
EN
In [5] we study Nonassociative Lambek Calculus (NL) augmented with De Morgan negation, satisfying the double negation and contraposition laws. This logic, introduced by de Grooté and Lamarche [10], is called Classical Non-Associative Lambek Calculus (CNL). Here we study a weaker logic InNL, i.e. NL with two involutive negations. We present a one-sided sequent system for InNL, admitting cut elimination. We also prove that InNL is PTIME.
4
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate

75%
Maffezioli P., Orlandelli E.
Bulletin of the Section of Logic
|
2019
|
tom 48
|
nr 2
137-158
EN
In previous work by Baaz and Iemhoff, a Gentzen calculus for intuitionistic logic with existence predicate is presented that satisfies partial cut elimination and Craig's interpolation property; it is also conjectured that interpolation fails for the implication-free fragment. In this paper an equivalent calculus is introduced that satisfies full cut elimination and allows a direct proof of interpolation via Maehara's lemma. In this way, it is possible to obtain much simpler interpolants and to better understand and (partly) overcome the failure of interpolation for the implication-free fragment.
5
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs

63%
Tourlakis G.
Bulletin of the Section of Logic
|
2016
|
tom 45
|
nr 1
EN
Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable. This paper applies the formulator approach to show the independence of the axiom schema ☐A → ☐∀ A of the logics M3and ML3 of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations.  In particular, the so modified ML3 is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics (compare with the more complexproofs in [2,8]).
6
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics

63%
Gao F., Tourlakis G.
Bulletin of the Section of Logic
|
2015
|
tom 44
|
nr 3-4
EN
A well established technique toward developing the proof theory of a Hilbert-style modal logic is to introduce a Gentzen-style equivalent (a Gentzenisation), then develop the proof theory of the latter, and finally transfer the metatheoretical results to the original logic (e.g., [1, 6, 8, 18, 10, 12]). In the first-order modal case, on one hand we know that the Gentzenisation of the straightforward first-order extension of GL, the logic QGL, admits no cut elimination (if the rule is included as primitive; or, if not included, then the rule is not admissible [1]). On the other hand the (cut-free) Gentzenisations of the first-order modal logics M3 and ML3 of [10, 12] do have cut as an admissible rule. The syntactic cut admissibility proof given in [18] for the Gentzenisation of the propositional provability logic GL is extremely complex, and it was the basis of the proofs of cut admissibility of the Gentzenisations of M3 and ML3, where the presence of quantifiers and quantifier rules added to the complexity and length of the proof. A recent proof of cut admissibility in a cut-free Gentzenisation of GL is given in [5] and is quite short and easy to read. We adapt it here to revisit the proofs for the cases of M3 and ML3, resulting to similarly short and easy to read proofs, only slightly complicated by the presence of quantification and its relevant rules.
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ć.