Informacja

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

English (EN)·Polski (PL)·Yкраїнський (UK)
Przejdź do strony domowej biblioteki Centralna Biblioteka Wojskowa Link otwiera się w nowym oknie Logo biblioteki Prolib Integro - strona głównaCentralna Biblioteka Wojskowa

Wyszukujesz frazę "CUT" wg kryterium: Temat

  Lista filtrów
Wyrównaj
    Wyświetlanie 1-15 z 15
    Tytuł:
    Analysis of Linear Regression Model at Divided System Matrix
    Analiza modelu regresji liniowej przy podzielonej macierzy układu
    Autorzy:
    Budka, Anna
    Wagner, Wiesław
    Powiązania:
    https://bibliotekanauki.pl/articles/906892.pdf
    Data publikacji:
    2007
    Wydawca:
    Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
    Tematy:
    linear regression model
    influential observations
    hat matrix
    complete
    1-cut and m-cut model
    Opis:
    In this study problems connected with the detection of influential observations are investigated in the linear regression model using the least squares estimation of structural parameters. This issue has been presented in three cuts: the complete model, 1-cut model and m-cut model.
    W pracy przedstawiono zagadnienia związane z wykrywaniem obserwacji wpływowych w modelu regresji liniowej przy zastosowaniu estymacji parametrów strukturalnych za pomocą MNK. Temat ten jest ujęty w trzech przekrojach: model pełny, 1-ucięty oraz model m-ucięty. W każdym przypadku prezentowane są szczegółowe metody badania obserwacji wpływowych. Podstawowymi dla tych celów statystykami są elementy diagonalne tzw. macierzy ortogonalnego rzutu. Ich duże wartości, przy czym wszystkie należą do przedziału (0, 1), przekraczające zadane wartości progowe pozwalają na wskazanie istnienia obserwacji wpływowych. Oczywiście różne możliwe statystyki będące w jakimś stopniu funkcjami elementów wspomnianej macierzy będą dostarczały informacji diagnostycznych o różnym znaczeniu, dotyczącym obserwacji wpływowych.
    Źródło:
    Acta Universitatis Lodziensis. Folia Oeconomica; 2007, 206
    0208-6018
    2353-7663
    Pojawia się w:
    Acta Universitatis Lodziensis. Folia Oeconomica
    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ł:
    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ł:
    Semantical Proof of Subformula Property for the Modal Logics K4.3, KD4.3, and S4.3
    Autorzy:
    Yazaki, Daishi
    Powiązania:
    https://bibliotekanauki.pl/articles/750044.pdf
    Data publikacji:
    2019
    Wydawca:
    Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
    Tematy:
    modal logic
    analytic cut
    subformula property
    finite model property
    Opis:
    The main purpose of this paper is to give alternative proofs of syntactical and semantical properties, i.e. the subformula property and the nite model property, of the sequent calculi for the modal logics K4.3, KD4.3, and S4.3. The application of the inference rules is said to be acceptable, if all the formulas in the upper sequents are subformula of the formulas in lower sequent. For some modal logics, Takano analyzed the relationships between the acceptable inference rules and semantical properties by constructing models. By using these relationships, he showed Kripke completeness and subformula property. However, his method is difficult to apply to inference rules for the sequent calculi for K4.3, KD4.3, and S4.3. Lookinglosely at Takano's proof, we nd that his method can be modied to construct nite models based on the sequent calculus for K4.3, if the calculus has (cut) and all the applications of the inference rules are acceptable. Similarly, we can apply our results to the calculi for KD4.3 and S4.3. This leads not only to Kripke completeness and subformula property, but also to finite model property of these logics simultaneously.
    Źródło:
    Bulletin of the Section of Logic; 2019, 48, 4
    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ł:
    An Investigation into Intuitionistic Logic with Identity
    Autorzy:
    Chlebowski, Szymon
    Leszczyńska-Jasion, Dorota
    Powiązania:
    https://bibliotekanauki.pl/articles/750046.pdf
    Data publikacji:
    2019
    Wydawca:
    Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
    Tematy:
    Non-Fregean logics
    intuitionistic logic
    admissibility of cut
    propositional identity
    congruence
    Opis:
    We define Kripke semantics for propositional intuitionistic logic with Suszko’s identity (ISCI). We propose sequent calculus for ISCI along with cut-elimination theorem. We sketch a constructive interpretation of Suszko’s propositional identity connective.
    Źródło:
    Bulletin of the Section of Logic; 2019, 48, 4
    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ł:
    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ł:
    Useful Four-Valued Extension of the Temporal Logic KtT4
    Autorzy:
    Degauquier, Vincent
    Powiązania:
    https://bibliotekanauki.pl/articles/749896.pdf
    Data publikacji:
    2018
    Wydawca:
    Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
    Tematy:
    temporal logic
    many-valued logic
    bi-intuitionistic logic
    paraconsistent logic
    sequent calculus
    duality
    cut-redundancy
    Opis:
    The temporal logic KtT4 is the modal logic obtained from the minimal temporal logic Kt by requiring the accessibility relation to be reflexive (which corresponds to the axiom T) and transitive (which corresponds to the axiom 4). This article aims, firstly, at providing both a model-theoretic and a proof-theoretic characterisation of a four-valued extension of the temporal logic KtT4 and, secondly, at identifying some of the most useful properties of this extension in the context of partial and paraconsistent logics.
    Źródło:
    Bulletin of the Section of Logic; 2018, 47, 1
    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-15 z 15

      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