?
On Lambek’s Restriction in the Presence of Exponential Modalities
P. 146-158.
Kanovich M., Kuznetsov S., Scedrov A.
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,” that is, 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 while keeping Lambek’s restriction. We present several versions of the Lambek calculus extended with exponential modalities and prove that those extensions are undecidable, even if we take only one of the two divisions provided by the Lambek calculus.
Publication based on the results of:
In book
Vol. 9537: Logical Foundations of Computer Science. , Springer, 2016
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
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
Max I. Kanovich, Mathematical Structures in Computer Science 2016 Vol. 26 No. 5 P. 719-744
In their seminal paper:
Lincoln, P., Mitchell, J., Scedrov, A. and Shankar, N. (1992). Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56 (1–3) 239–311,
LMSS have established an extremely surprising result that propositional linear logic is undecidable. Their proof is very complex and involves numerous nested inductions of different kinds.
Later an alternative ...
Added: September 1, 2016
Kanovich M., Kuznetsov S., Scedrov A., , in : Logic, Language, Information, and Computation: 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, Proceedings. Vol. 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
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
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., 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
Slavnov S. A., Theoretical Computer Science 2006 Vol. 357 No. 1-3 P. 215-229
Added: March 4, 2013
Rybakov M., Shkatov D., , in : Advances in Modal Logic. Vol. 13.: College Publications, 2020. P. 523-539.
We study algorithmic properties of first-order predicate monomodal logics of the natural number line in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. The languages we consider have no constants, function symbols, or the equality symbol. We show that satisfiability for the logics of is not arithmitical in languages ...
Added: August 27, 2020
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., Ban Kirigin T., Nigam V. et al., Computer Languages, Systems & Structures 2014 No. 40 P. 137-154
It is well-known that the Dolev–Yao adversary is a powerful adversary. Besides acting as the network, intercepting, decomposing, composing and sending messages, he can remember as much information as he needs. That is, his memory is unbounded. We recently proposed a weaker Dolev–Yao like adversary, which also acts as the network, but whose memory is ...
Added: March 23, 2015
Sergey Slavnov, Mathematical Structures in Computer Science 2021 Vol. 31 No. 5 P. 495-534
Ehrhard et al. (2018. Proceedings of the ACM on Programming Languages, POPL 2, Article 59.) proposed a model of probabilistic functional programming in a category of normed positive cones and stable measurable cone maps, which can be seen as a coordinate-free generalization of probabilistic coherence spaces (PCSs). However, unlike the case of PCSs, it remained unclear ...
Added: November 16, 2021
Zolin E., Journal of Logic and Computation 2017 Vol. 27 No. 5 P. 1399-1420
We extend the language of the modal logic K4 of transitive frames with two sorts of modalities. In addition to the usual possibility modality (which means that a formula holds in some successor of a given point), we consider graded modalities (a formula holds in at least n successors) and converse graded modalities (aformula holds ...
Added: June 14, 2018
Rybakov M., Shkatov D., Journal of Logic and Computation 2020 Vol. 30 No. 7 P. 1305-1329
We study the effect of restricting the number of individual variables, as well as the number and arity of predicate letters, in languages of first-order predicate modal logics of finite Kripke frames on the logics’ algorithmic properties. A finite frame is a frame with a finite set of possible worlds. The languages we consider have ...
Added: August 27, 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, Proceedings. Vol. 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
Sergey Slavnov, Logical Methods in Computer Science 2019 Vol. 15 No. 3 P. 1-25
Pomset logic introduced by Retoré is an extension of linear logic with a self-dual noncommutative connective. The logic is defined by means of proof-nets, rather than a sequent calculus. Later a deep inference system BV was developed with an eye to capturing Pomset logic, but equivalence of system has not been proven up to now. ...
Added: October 23, 2019
Savateev Y., Известия РАН. Серия математическая 2011 Т. 75 № 3 С. 189-222
We use proof-nets to study the algorithmic complexity of the derivability problem for some fragments of the Lambek calculus. We prove the NP-completeness of this problem for the unidirectional fragment and the product-free fragment, and also for versions of these fragments that admit empty antecedents. ...
Added: October 20, 2014
Blaisdell E., Kanovich M., Stepan L. Kuznetsov et al., , in : Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, Proceedings. Vol. 13385.: Cham : Springer, 2022. P. 449-467.
Added: August 7, 2022
Sergey Slavnov, / Cornell University. Series arXiv "math". 2016.
We study the question when a $*$-autonomous Mix-category has a representation as a $*$-autonomous Mix-subcategory of a compact one. We define certain partial trace-like operation on morphisms of a Mix-category, which we call a mixed trace, and show that any structure preserving embedding of a Mix-category into a compact one induces a mixed trace on ...
Added: November 23, 2016
Sergey Slavnov, Journal of Cognitive Science 2021 Vol. 22 No. 2 P. 68-91
We propose a concrete surface representation of abstract categorial grammars in the category of word cobordisms or cowordisms
for short, which are certain bipartite graphs decorated withwords in a given alphabet, generalizing linear logic proof-nets.
We also introduce and study linear logic grammars, directly based on cobordisms and using classical multiplicative linear logic
as a typing system. ...
Added: October 2, 2021
Blute R., Panangaden P., Slavnov Sergey, Applied Categorical Structures 2012 Vol. 20 No. 3 P. 209-228
This paper proposes a definition of categorical model of the deep inference system BV, defined by Guglielmi. Deep inference introduces the idea of performing a deduction in the interior of a formula, at any depth. Traditional sequent calculus rules only see the roots of formulae. However in these new systems, one can rewrite at any ...
Added: February 18, 2013
Rybakov M., Shkatov D., Studia Logica 2019 Vol. 107 No. 4 P. 695-717
We prove that the positive fragment of first-order intuitionistic logic in the language with two individual variables and a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals [QBL;QKC] and [QBL;QFL], where QKC ...
Added: October 2, 2019
Kontchakov R., Pratt-Hartmann I., Nenov Y. et al., ACM Transactions on Computational Logic 2013 Vol. 14 No. 2 P. 13.1-13.48
We consider the quantifier-free languages, Bc and Bc°, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of Rn (n ≥ 2) and, additionally, over the regular closed ...
Added: March 25, 2015