Informacja

Drogi użytkowniku, aplikacja do prawidłowego działania wymaga obsługi JavaScript. Proszę włącz obsługę JavaScript w Twojej przeglądarce.

Wyszukujesz frazę "cut elimination" wg kryterium: Temat


Wyświetlanie 1-11 z 11
Tytuł:
Rule-Generation Theorem and its Applications
Autorzy:
Indrzejczak, Andrzej
Powiązania:
https://bibliotekanauki.pl/articles/749922.pdf
Data publikacji:
2018
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
sequent calculus
cut elimination
proof theory
extralogical rules
Opis:
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.
Źródło:
Bulletin of the Section of Logic; 2018, 47, 4
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
Cut Elimination Theorem for Non-Commutative Hypersequent Calculus
Autorzy:
Indrzejczak, Andrzej
Powiązania:
https://bibliotekanauki.pl/articles/749932.pdf
Data publikacji:
2017
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
temporal logic
linear time
hypersequent calculus
cut elimination
Opis:
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.
Źródło:
Bulletin of the Section of Logic; 2017, 46, 1/2
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
Labeled Sequent Calculus for Orthologic
Autorzy:
Kawano, Tomoaki
Powiązania:
https://bibliotekanauki.pl/articles/749930.pdf
Data publikacji:
2018
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
quantum logic
sequent calculus
cut-elimination theorem
decidability
Kripke model
Opis:
Orthologic (OL) is non-classical logic and has been studied as a part of quantumlogic. OL is based on an ortholattice and is also called minimal quantum logic. Sequent calculus is used as a tool for proof in logic and has been examinedfor several decades. Although there are many studies on sequent calculus forOL, these sequent calculi have some problems. In particular, they do not includeimplication connective and they are mostly incompatible with the cut-eliminationtheorem. In this paper, we introduce new labeled sequent calculus called LGOI, and show that this sequent calculus solve the above problems. It is alreadyknown that OL is decidable. We prove that decidability is preserved when theimplication connective is added to OL.
Źródło:
Bulletin of the Section of Logic; 2018, 47, 4
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
Cut Elimination for Extended Sequent Calculi
Autorzy:
Martini, Simone
Masini, Andrea
Zorzi, Margherita
Powiązania:
https://bibliotekanauki.pl/articles/43182562.pdf
Data publikacji:
2023
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
proof theory
sequent calculus
cut elimination
modal logic
2-sequents
Opis:
We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \(\Box\) and \(\Diamond\). Starting points for this research are 2-sequents and indexed-based calculi (sequents and tableaux). By extending and modifying existing proposals, we show how to achieve a syntactical proof of the cut-elimination theorem that is as close as possible to the one for first-order classical logic. In doing this, we implicitly show how small is the proof-theoretical distance between classical logic and the systems under consideration.
Źródło:
Bulletin of the Section of Logic; 2023, 52, 4; 459-495
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
Autorzy:
Maffezioli, Paolo
Orlandelli, Eugenio
Powiązania:
https://bibliotekanauki.pl/articles/749910.pdf
Data publikacji:
2019
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
intuitionistic logic
existence predicate
sequent calculi
cut elimination
interpolation
Maehara's lemma
Opis:
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.
Źródło:
Bulletin of the Section of Logic; 2019, 48, 2; 137-158
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity
Autorzy:
Buszkowski, Wojciech
Powiązania:
https://bibliotekanauki.pl/articles/749946.pdf
Data publikacji:
2017
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
nonassociative Lambek calculus
linear logic
sequent system
cut elimination
PTIME complexity
Opis:
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.
Źródło:
Bulletin of the Section of Logic; 2017, 46, 1/2
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
Autorzy:
Braüner, Torben
Powiązania:
https://bibliotekanauki.pl/articles/2142755.pdf
Data publikacji:
2022-01-07
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
hybrid logic
natural deduction systems
sequent systems
normalization
cut-elimination
analycity
Opis:
This paper is about non-labelled proof-systems for hybrid logic, that is, proofsystems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that nonlabelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations.
Źródło:
Bulletin of the Section of Logic; 2022, 51, 2; 143-162
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
Linear Abelian Modal Logic
Autorzy:
Mohammadi, Hamzeh
Powiązania:
https://bibliotekanauki.pl/articles/43184005.pdf
Data publikacji:
2024
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
many-valued logic
modal logic
abelian logic
hypersequent calculus
cut-elimination
Opis:
A many-valued modal logic, called linear abelian modal logic \(\rm {\mathbf{LK(A)}}\) is introduced as an extension of the abelian modal logic \(\rm \mathbf{K(A)}\). Abelian modal logic \(\rm \mathbf{K(A)}\) is the minimal modal extension of the logic of lattice-ordered abelian groups. The logic \(\rm \mathbf{LK(A)}\) is axiomatized by extending \(\rm \mathbf{K(A)}\) with the modal axiom schemas \(\Box(\varphi\vee\psi)\rightarrow(\Box\varphi\vee\Box\psi)\) and \((\Box\varphi\wedge\Box\psi)\rightarrow\Box(\varphi\wedge\psi)\). Completeness theorem with respect to algebraic semantics and a hypersequent calculus admitting cut-elimination are established. Finally, the correspondence between hypersequent calculi and axiomatization is investigated.
Źródło:
Bulletin of the Section of Logic; 2024, 53, 1; 1-28
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics
Autorzy:
Gao, Feng
Tourlakis, George
Powiązania:
https://bibliotekanauki.pl/articles/749884.pdf
Data publikacji:
2015
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
Modal logic
GL
QGL
first-order logic
proof theory
cut elimination
cut admissibility
provability logic
Opis:
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.
Źródło:
Bulletin of the Section of Logic; 2015, 44, 3-4
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\)
Autorzy:
Ayhan, Sara
Wansing, Heinrich
Powiązania:
https://bibliotekanauki.pl/articles/43181589.pdf
Data publikacji:
2023
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
bilateralism
bi-intuitionistic logic \(\mathtt{2Int}\)
cut-elimination
identity of derivations
synonymy
Opis:
We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus \(\mathtt{SC2Int}\) for the bi-intuitionistic logic \(\mathtt{2Int}\). A distinctive feature of \(\mathtt{SC2Int}\) is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of \(\mathtt{SC2Int}\), in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, mediated through two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of \(\mathtt{2Int}\). By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in \(\mathtt{SC2Int}\) is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously.
Źródło:
Bulletin of the Section of Logic; 2023, 52, 2; 187-237
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs
Autorzy:
Tourlakis, George
Powiązania:
https://bibliotekanauki.pl/articles/749974.pdf
Data publikacji:
2016
Wydawca:
Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Tematy:
Modal logic
GL
first-order logic
proof theory
cut elimination
reflection property
disjunction property
quantified modal logic
QGL
arithmetical completeness
Opis:
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]).
Źródło:
Bulletin of the Section of Logic; 2016, 45, 1
0138-0680
2449-836X
Pojawia się w:
Bulletin of the Section of Logic
Dostawca treści:
Biblioteka Nauki
Artykuł
    Wyświetlanie 1-11 z 11

    Ta witryna wykorzystuje pliki cookies do przechowywania informacji na Twoim komputerze. Pliki cookies stosujemy w celu świadczenia usług na najwyższym poziomie, w tym w sposób dostosowany do indywidualnych potrzeb. Korzystanie z witryny bez zmiany ustawień dotyczących cookies oznacza, że będą one zamieszczane w Twoim komputerze. W każdym momencie możesz dokonać zmiany ustawień dotyczących cookies