Temat: cut-elimination - Prolib Integro

Skocz do pozycji: 1.

Tytuł:: Rule-Generation Theorem and its Applications
Autorzy:: Indrzejczak, Andrzej
Tematy:: sequent calculus
cut elimination
proof theory
extralogical rules; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/749922.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 2.

Tytuł:: Cut Elimination Theorem for Non-Commutative Hypersequent Calculus
Autorzy:: Indrzejczak, Andrzej
Tematy:: temporal logic
linear time
hypersequent calculus
cut elimination; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/749932.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 3.

Tytuł:: Labeled Sequent Calculus for Orthologic
Autorzy:: Kawano, Tomoaki
Tematy:: quantum logic
sequent calculus
cut-elimination theorem
decidability
Kripke model; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/749930.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 4.

Tytuł:: Cut Elimination for Extended Sequent Calculi
Autorzy:: Martini, Simone
Masini, Andrea
Zorzi, Margherita
Tematy:: proof theory
sequent calculus
cut elimination
modal logic
2-sequents; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/43182562.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 5.

Tytuł:: Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
Autorzy:: Maffezioli, Paolo
Orlandelli, Eugenio
Tematy:: intuitionistic logic
existence predicate
sequent calculi
cut elimination
interpolation
Maehara's lemma; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/749910.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 6.

Tytuł:: Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity
Autorzy:: Buszkowski, Wojciech
Tematy:: nonassociative Lambek calculus
linear logic
sequent system
cut elimination
PTIME complexity; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/749946.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 7.

Tytuł:: Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
Autorzy:: Braüner, Torben
Tematy:: hybrid logic
natural deduction systems
sequent systems
normalization
cut-elimination
analycity; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/2142755.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 8.

Tytuł:: Linear Abelian Modal Logic
Autorzy:: Mohammadi, Hamzeh
Tematy:: many-valued logic
modal logic
abelian logic
hypersequent calculus
cut-elimination; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/43184005.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 9.

Tytuł:: On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\)
Autorzy:: Ayhan, Sara
Wansing, Heinrich
Tematy:: bilateralism
bi-intuitionistic logic \(\mathtt{2Int}\)
cut-elimination
identity of derivations
synonymy; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/43181589.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Skocz do pozycji: 10.

Tytuł:: A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics
Autorzy:: Gao, Feng
Tourlakis, George
Tematy:: Modal logic
GL
QGL
first-order logic
proof theory
cut elimination
cut admissibility
provability logic; Pokaż więcej
Wydawca:: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
Powiązania:: https://bibliotekanauki.pl/articles/749884.pdf Link otwiera się w nowym oknie
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.
Dostawca treści:: Biblioteka Nauki

Artykuł

na półce

Informacja

Wyszukujesz frazę "cut-elimination" wg kryterium: Temat