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 Pedagogiczna Biblioteka Wojewódzka im. Komisji Edukacji Narodowej w Lublinie Link otwiera się w nowym oknie Logo biblioteki Prolib Integro - strona głównaPedagogiczna Biblioteka Wojewódzka im. Komisji Edukacji Narodowej w Lublinie
Zmień bibliotekę

Wyszukujesz frazę "linear logic" wg kryterium: Temat

  Lista filtrów
Wyrównaj
    Wyświetlanie 1-10 z 10
    Tytuł:
    Linear logic in computer science
    Autorzy:
    Steingartner, W.
    Poláková, A.
    Prazňák, P.
    Novitzká, V.
    Tematy:
    linear logic
    resources
    proofs
    Pokaż więcej
    Wydawca:
    Politechnika Częstochowska. Wydawnictwo Politechniki Częstochowskiej
    Powiązania:
    https://bibliotekanauki.pl/articles/122583.pdf  Link otwiera się w nowym oknie
    Opis:
    Linear logic has many properties that make it suitable for application in various areas of computer science. It is able to describe dynamic processes, non-determinism, parallelism on syntactic level. In our paper we try to discuss resource oriented character of linear logic, its possibility to deal with such important resources for computer science as space (memory) and time. Handling with resources takes place in deduction system of linear logic. We show how special form of proofs, called designs, is constructed and we show the relationship between space and time in designs.
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
    Autorzy:
    Płaczek, Paweł
    Tematy:
    Substructural logic
    Lambek calculus
    nonassociative linear logic
    sequent system
    PTime complexity
    Pokaż więcej
    Wydawca:
    Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
    Powiązania:
    https://bibliotekanauki.pl/articles/1023344.pdf  Link otwiera się w nowym oknie
    Opis:
    Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime complexity of the multiplicative fragment of NBL.
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    A categorical model of predicate linear logic
    Autorzy:
    Demeterová, E.
    Mihályi, D.
    Novitzká, V.
    Tematy:
    linear type theory
    predicate linear logic
    symmetric monoidal closed category
    Pokaż więcej
    Wydawca:
    Politechnika Częstochowska. Wydawnictwo Politechniki Częstochowskiej
    Powiązania:
    https://bibliotekanauki.pl/articles/122570.pdf  Link otwiera się w nowym oknie
    Opis:
    Linear logic is one of the logical systems with special properties suitable for describing real processes used in computer science. It enables one to specify dynamics, non determinism, consecutive processes and important resources as memory and time on syntactic level. Moreover, its deduction system enables one to verify specified properties. Constructing an appropriate model based on categories can serve for modeling various program systems in the wide spectrum of computer science. Mainly, propositional linear logic is used for these purposes. The expression power of linear logic significantly grows by extending propositional logic with predicates and quantifiers. Our paper concerns itself with defining predicate linear logic together with its deduction system and our main aim is to construct a categorical model of predicate linear logic as a symmetric monoidal closed category.
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    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ł
    Tytuł:
    Sequent Systems for Consequence Relations of Cyclic Linear Logics
    Autorzy:
    Płaczek, Paweł
    Tematy:
    linear logic
    Lambek calculus
    nonassociative logics
    noncommutative logics
    substructural logics
    consequence relation
    nonlogical axioms
    conservativeness
    Pokaż więcej
    Wydawca:
    Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
    Powiązania:
    https://bibliotekanauki.pl/articles/43186342.pdf  Link otwiera się w nowym oknie
    Opis:
    Linear Logic is a versatile framework with diverse applications in computer science and mathematics. One intriguing fragment of Linear Logic is Multiplicative-Additive Linear Logic (MALL), which forms the exponential-free component of the larger framework. Modifying MALL, researchers have explored weaker logics such as Noncommutative MALL (Bilinear Logic, BL) and Cyclic MALL (CyMALL) to investigate variations in commutativity. In this paper, we focus on Cyclic Nonassociative Bilinear Logic (CyNBL), a variant that combines noncommutativity and nonassociativity. We introduce a sequent system for CyNBL, which includes an auxiliary system for incorporating nonlogical axioms. Notably, we establish the cut elimination property for CyNBL. Moreover, we establish the strong conservativeness of CyNBL over Full Nonassociative Lambek Calculus (FNL) without additive constants. The paper highlights that all proofs are constructed using syntactic methods, ensuring their constructive nature. We provide insights into constructing cut-free proofs and establishing a logical relationship between CyNBL and FNL.
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Between syntax and semantics of resource oriented logic for ids behavior description
    Autorzy:
    Perhac, J.
    Mihalyi, D.
    Novitzka, V.
    Tematy:
    intrusion detection system
    linear logic
    Kripke’s semantics
    ludics
    bezpieczeństwo sieci
    system wykrywania włamań
    logika liniowa
    semantyka Kripke
    Pokaż więcej
    Wydawca:
    Politechnika Częstochowska. Wydawnictwo Politechniki Częstochowskiej
    Powiązania:
    https://bibliotekanauki.pl/articles/122478.pdf  Link otwiera się w nowym oknie
    Opis:
    Linear logic appears as a suitable logical system for description of dynamic properties of various network activities in computer science. It disposes with new connectives which create new opportunities to describe properties of real network processes, e.g. parallelism, causality and commutativity of duality between processes. We extend this logic with Aristotelian modalities and we formulate their appropriate model. In our contribution we show how a real network attack can be formalized in this logical system as a polarized game.
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Paraconsistent sequential linear-time temporal logic : combining paraconsistency and sequentiality in temporal reasoning
    Autorzy:
    Kamide, Norihiro
    Tematy:
    linear-time temporal logic
    paraconsistent logic
    sequent calculus
    Pokaż więcej
    Wydawca:
    Uniwersytet Jagielloński. Wydawnictwo Uniwersytetu Jagiellońskiego
    Powiązania:
    https://bibliotekanauki.pl/articles/61523585.pdf  Link otwiera się w nowym oknie
    Opis:
    Inconsistency-tolerant temporal reasoning with sequential (i.e., ordered or hierarchical) information is gaining in- creasing importance in computer science applications. A logical system for representing such reasoning is thus required for ob- taining a theoretical basis for such applications. In this paper, we introduce a new logic called paraconsistent sequential linear-time temporal logic (PSLTL), which is an extension of the standard linear-time temporal logic (LTL). PSLTL can appropriately rep- resent inconsistency-tolerant temporal reasoning with sequential information. The cut-elimination, decidability, and completeness theorems for PSLTL are proved in this paper.
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Application of deductive reasoning to the verification of archimate behavioral elements
    Autorzy:
    Klimek, Radosław
    Szwed, Piotr
    Jędrusik, Stanisław
    Tematy:
    Deductive temporal reasoning
    software verification
    ArchiMate
    semantics table¬aux method
    Linear Temporal Logic
    Pokaż więcej
    Wydawca:
    Wydawnictwo Uniwersytetu Ekonomicznego we Wrocławiu
    Powiązania:
    https://bibliotekanauki.pl/articles/431909.pdf  Link otwiera się w nowym oknie
    Opis:
    The formal verification of business models has recently become an intensively researched area. It is expected that the application of formal tools may bring such benefits to organizations as the improved quality of products and services and a lower ratio of operational errors. In this paper we discuss the application of a deduction-based method for the verification of the behavioral aspects of ArchiMate models. The first step in our method consists in the translation of the ArchiMate model into Linear Temporal Logic (LTL) formulas. The resulting LTL formulas are then verified to check the expected temporal properties. The verification process is based on the semantics tableaux method and is conducted with an LTL prover. The method is discussed using an example of a business process implemented within a surveillance system.
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    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ł
    Tytuł:
    Motion control system of autonomous mobile robot
    System sterowania ruchem autonomicznego robota mobilnego
    Autorzy:
    Tsmots, I.
    Vavruk, I.
    Tkachenko, R.
    Tematy:
    robot mobilny
    system sterowania ruchem
    logika rozmyta
    regresja liniowa
    mobile robot
    motion control system
    fuzzy logic
    linear regression
    Pokaż więcej
    Wydawca:
    Politechnika Lubelska. Wydawnictwo Politechniki Lubelskiej
    Powiązania:
    https://bibliotekanauki.pl/articles/407642.pdf  Link otwiera się w nowym oknie
    Opis:
    In this article the motion control system of autonomous mobile robot is described. Four motion modes: motion mode “to the target”, motion mode “obstacles avoidance”, motion mode “along the right wall” and motion mode “along the left wall” are implemented. A method for determining the effective rotation angle of mobile robot which is a linear combination of rotation angles which are obtained in different motion modes and activation coefficients is proposed. Fuzzy-oriented method with high accuracy and performance is used for motion modes implementation and for finding values of activation coefficients.
    W artykule opisano system sterowania ruchem autonomicznego robota mobilnego. Zaimplementowano cztery tryby ruchu: „do celu”, „unikanie przeszkód”, „wzdłuż prawej ściany” oraz „wzdłuż lewej ściany”. Zaproponowano metodę do określania efektywnego kąta obrotu robota, która jest liniową kombinacją kąta obrotu, który jest otrzymywany dla różnych trybów ruchu oraz współczynników aktywacji. Do implementacji trybów pracy oraz znalezienia wartości współczynników aktywacji użyto metodę rozmytą o dużej dokładności i wydajności.
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
      Wyświetlanie 1-10 z 10

      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