?
A Logical Framework with Commutative and Non-commutative Subexponentials
P. 228–245.
Logical frameworks allow the specification of deductive systems using the same logical machinery. Linear logical frameworks have been successfully used for the specification of a number of computational, logics and proof systems. Its success relies on the fact that formulas can be distinguished as linear, which behave intuitively as resources, and unbounded, which behave intuitionistically. Commutative subexponentials enhance the expressiveness of linear logic frameworks by allowing the distinction of multiple contexts. These contexts may behave as multisets of formulas or sets of formulas. Motivated by applications in distributed systems and in type-logical grammar, we propose a linear logical framework containing both commutative and non-commutative subexponentials. Non-commutative subexponentials can be used to specify contexts which behave as lists, not multisets, of formulas. In addition, motivated by our applications in type-logical grammar, where the weakenening rule is disallowed, we investigate the proof theory of formulas that can only contract, but not weaken. In fact, our contraction is non-local. We demonstrate that under some conditions such formulas may be treated as unbounded formulas, which behave intuitionistically.
Publication based on the results of:
In book
Issue 10900. , Springer International Publishing AG, part of Springer Nature 2018, 2018.
Stepan L. Kuznetsov, Journal of Logic and Computation 2026 Vol. 36 No. 1 Article exaf078
The linguistic applications of the Lambek calculus suggest its semantics over algebras of formal languages. A straightforward approach to construct such semantics indeed yields a brilliant completeness theorem (Pentus 1995, Ann. Pure Appl. Logic, 75, 179–213). However, extending the calculus with extra operations ruins completeness. In order to mitigate this issue, Wurm (2017, J. Logic Lang. Inf., ...
Added: January 14, 2026
Kuznetsov S., Speranski S. O., Annals of Pure and Applied Logic 2022 Vol. 173 No. 2 Article 103057
We introduce infinitary action logic with exponentiation — that is, the multiplicative-additive Lambek calculus extended with Kleene star and with a family of subexponential modalities, which allow some of the structural rules (contraction, weakening, permutation). The logic is presented in the form of an infinitary sequent calculus. We prove cut elimination and, in the case ...
Added: December 26, 2025
Kuznetsov S., Speranski S. O., Studia Logica 2023 Vol. 111 No. 2 P. 251–280
Infinitary action logic can be naturally expanded by adding exponential and subexponential modalities from linear logic. In this article we shall develop infinitary action logic with a subexponential that allows multiplexing (instead of contraction). Both non-commutative and commutative versions of this logic will be considered, presented as infinitary sequent calculi. We shall prove cut admissibility ...
Added: December 26, 2025
Fedyanin D., , in: 17th International Conference, SCSM 2025, Held as Part of the 27th HCI International Conference, HCII 2025, Gothenburg, Sweden, June 22–27, 2025, Proceedings, Part II. Social Computing and Social Media. LNCS, volume 15787Vol. 2.: Switzerland: Springer, 2025. P. 247–256.
The paper proposes a formal model for describing opinions and higher-order opinions (e.g., opinions about opinions) using classical epistemic logic, such as the Kripke structure. Traditionally employed for analyzing knowledge and beliefs, this model is adapted to interpret opinions as beliefs, which is particularly promising for describing human-computer interaction due to its high level of formalization. The study is ...
Added: December 13, 2025
Kuznetsov S., Lugovaya V., Ryzhova A., Logic Journal of the IGPL 2019 Vol. 27 No. 3 P. 252–266
Added: May 1, 2025
Lesiv B., Антиномии 2024 Т. 24 № 2 С. 107–139
Подход к праву, разработанный известным американским судьей О. Холмсом, остается малоизученным в России по ряду причин методологического характера. Одна из них заключается в том, что исследования не предваряются целенаправленной концептуализацией формализма как общего импульса, побудившего американское юридическое сообщество XIX–XX вв. рассматривать юридическую практику с точки зрения новых ценностей. Реалистический подход к праву зародился не в ...
Added: August 6, 2024
Stepan L. Kuznetsov, , in: Logic, Language, Information, and Computation: 30th International Workshop, WoLLIC 2024, Bern, Switzerland, June 10–13, 2024, ProceedingsVol. 14672: Lecture Notes in Computer Science.: Cham: Springer, 2024. P. 93–107.
Added: June 12, 2024
Sergey Slavnov, Logical Methods in Computer Science 2023 Vol. 19 No. 4
It is known that different categorial grammars have surface representation in a fragment of first order multiplicative linear logic (MLL1). We show that the fragment of interest is equivalent to the recently introduced extended tensor type calculus (ETTC). ETTC is a calculus of specific typed terms, which represent tuples of strings, more precisely bipartite graphs ...
Added: December 20, 2023
S. M. Dudakov, Karlov B. N., S. L. Kuznetsov et al., Algebra and Logic 2021 Vol. 60 No. 5 P. 308–326
The Lambek calculus with the unit can be defined as the atomic theory (algebraic logic) of the class of residuated monoids. This calculus, being a theory of a broader class of algebras than Heyting ones, is weaker than intuitionistic logic. Namely, it lacks structural rules: permutation, contraction, and weakening. We consider two extensions of the ...
Added: November 12, 2023
Kanovich M., Kuznetsov Stepan G., Kuznetsov S. et al., Studies in Computational Intelligence 2021 Vol. 999 P. 1–24
CatLog is a categorial grammar parser/theorem-prover
developed by Glyn Morrill and his co-authors. CatLog is based on an
extension of Lambek calculus. A distinctive feature of this extension is
the usage of brackets for controlled non-associativity and a subexponential
modality whose contraction rule interacts with bracketing in a
sophisticated way. We consider two variants of the calculus, appearing in
different versions ...
Added: December 14, 2021
Kanovich M., Kuznetsov S., Scedrov A., Information and Computation 2022 Vol. 287 Article 104760
We investigate language interpretations of two extensions of the Lambek calculus: with additive conjunction and disjunction and with additive conjunction and the unit constant. For extensions with additive connectives, we show that conjunction and disjunction behave differently. Adding both of them leads to incompleteness due to the distributivity law. We show that with conjunction only ...
Added: December 4, 2021
Slavnov S. A., Journal of Logic and Computation 2022 Vol. 32 No. 3 P. 479–517
We consider tensor grammars, which are an example of ‘commutative’ grammars, based on the classical (rather than intuitionistic) linear logic. They can be seen as a surface representation of abstract categorial grammars (ACG) in the sense that derivations of ACG translate to derivations of tensor grammars and this translation is isomorphic on the level of string ...
Added: October 21, 2021
Kanovich M., Kuznetsov S., Scedrov A., Journal of Logic, Language and Information 2021 Vol. 30 No. 1 P. 31–88
We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill’s calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the ! subexponential modality. For ...
Added: November 25, 2020
Kuznetsov S., , in: Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th BirthdayIssue 12300.: Cham: Springer, 2020. P. 3–16.
Infinitary action logic is an extension of the multiplicative-additive Lambek calculus with Kleene iteration, axiomatized by an 𝜔-rule. Buszkowski and Palka (2007) show that this logic is \(\Pi^0_1\)-complete. As shown recently by Kuznetsov and Speranski, the extension of infinitary action logic with the exponential modality is much harder: \(\Pi^1_1\)-complete. The raise of complexity is of ...
Added: November 25, 2020
Kanovich M., Kuznetsov S., Scedrov A., Journal of Logic and Computation 2020 Vol. 30 No. 1 P. 239–256
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality ...
Added: July 1, 2020
Kanovich M., Kuznetsov S., Scedrov A., , in: Logic, Language, Information, and Computation: 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, ProceedingsVol. 11541: Lecture Notes in Computer Science.: Berlin, Heidelberg: Springer, 2019. P. 356–372.
The Lambek calculus was introduced as a mathematical description of natural languages. The original Lambek calculus is NP-complete (Pentus), while its product-free fragment with only one implication is polynomially decidable (Savateev). We consider Lambek calculus with the additional connectives: conjunction and disjunction. It is known that this system is PSPACE-complete (Kanovich, Kanazawa). We prove, in ...
Added: September 4, 2019
Kanovich M., Kuznetsov S., Scedrov A., , in: Logic, Language, Information, and Computation: 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, ProceedingsVol. 11541: Lecture Notes in Computer Science.: Berlin, Heidelberg: Springer, 2019. P. 373–391.
Language and relational models, or L-models and R-models, are two natural classes of models for the Lambek calculus. Completeness w.r.t. L-models was proved by Pentus and completeness w.r.t. R-models by Andréka and Mikulás. It is well known that adding both additive conjunction and disjunction together yields incompleteness, because of the distributive law. The product-free Lambek ...
Added: September 4, 2019
Demin M., History and Philosophy of Logic 2019 Vol. 40 No. 4 P. 374–388
During the nineteenth century, German philosophy developed from a type of general knowledge to an academic discipline at the university. Changes across disciplines to the philosophy of science and psychological surveys created new challenges for the place and purpose of philosophy in the educational system. The content of logic courses for secondary schools (Gymnasiums) was ...
Added: August 12, 2019
Springer International Publishing AG, part of Springer Nature 2018, 2018.
9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings ...
Added: July 11, 2018
Avdoshin S. M., Набебин А. А., М.: ДМК Пресс, 2018.
The textbook contains the basic information of formal logical systems. It is Boolean functions, Post’s theorem on functional completeness, the k-valued logic, derivatives of Boolean functions, axiomatic calculi for propositions, for predicates, for sequentions, for resolutions. Programming language Prolog and axiomatic programming language OBJ3 are introduced. Problems of monadic logic, of finite automata and of ...
Added: December 2, 2017
Kanovich M., Kuznetsov S., Morrill G. et al., , in: Second International Conference on Formal Structures for Computation and Deduction, FSCD 2017Vol. 84: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017).: [б.и.], 2017. P. 22:1–22:17.
Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. Pentus (2010) gave a polynomial-time algorithm for determining provability of bounded depth formulas in L* , the Lambek calculus with empty antecedents allowed. Pentus’ algorithm is based on tabularisation of proof nets. Lambek calculus with ...
Added: September 15, 2017
[б.и.], 2017.
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) ...
Added: September 15, 2017
Kanovich M., Scedrov A., Kuznetsov S., , in: 21st International Symposium, Fundamentals of Computation Theory 2017, FCT 2017.: Springer, 2017. P. 326–340.
The Lambek calculus is a well-known logical formalism for modelling natural language syntax. The original calculus covered a substantial number of intricate natural language phenomena, but only those restricted to the context-free setting. In order to address more subtle linguistic issues, the Lambek calculus has been extended in various ways. In particular, Morrill and Valentín ...
Added: September 14, 2017