?
Undecidability of a newly proposed calculus for CatLog3
P. 67-83.
In his recent papers “Parsing/theorem-proving for logical grammar CatLog3” and “A note on movement in logical grammar”, Glyn Morrill proposes a new substructural calculus to be used as the basis for the categorial grammar parser CatLog3. In this paper we prove that the derivability problem for a fragment of this calculus is algorithmically undecidable.
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
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., 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
Rybakov M., University of the Witwatersrand, Johannesburg, 2019
Modal logics, both propositional and predicate, have been used in computer science since the late 1970s. One of the most important properties of modal logics of relevance to their applications in computer science is the complexity of their satisfiability problem. The complexity of satisfiability for modal logics is rather high: it ranges from NP-complete to ...
Added: October 5, 2019
Kuznetsov S., , in : 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019). : IEEE, 2019. Ch. 36. P. 1-9.
We prove algorithmic undecidability of the (in)equational theory of residuated Kleene lattices (action lattices), thus solving a problem left open by D. Kozen, P. Jipsen, W. Buszkowski. ...
Added: September 4, 2019
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
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
Salibekyan, S., Panfilov, P., , in : Supplementary Proceedings of the Sixth International Conference on Analysis of Images, Social Networks and Texts (AIST-SUP 2017), Moscow, Russia, July 27-29, 2017. Vol. 1975.: Aachen : CEUR-WS.org, 2017. P. 134-145.
In this paper, we present an object-attribute grammar (OAG) – an original formalism for describing the natural language semantic analysis algorithm for the linguistic processor (LP). Special focus is made on formatting input and output data for LP. The LP uses the graph containing word interpretations of source text and transforms it to the graph ...
Added: June 21, 2018
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 S., Scedrov A., , in : Symposium on Logical Foundations of Computer Science (LFCS 2016). Vol. 9537: Logical Foundations of Computer Science.: Springer, 2016. P. 146-158.
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 ...
Added: June 28, 2016
Rybakov M., Shkatov D., Logic Journal of the IGPL 2022 Vol. 30 No. 3 P. 519-533
We obtain an effective embedding of the classical predicate logic into the logic of partial quasiary predicates. The embedding has the property that an image of a non-theorem of the classical logic is refutable in a model of the logic of partial quasiary predicates that has the same cardinality as the classical countermodel of the ...
Added: May 29, 2021
Brotherston J., Kanovich M., Journal of the ACM 2014 Vol. 61 No. 2 P. 14:1-14:43
In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism ...
Added: March 23, 2015
Kanovich M., Kuznetsov S., Morrill G. et al., , in : Second International Conference on Formal Structures for Computation and Deduction, FSCD 2017. Vol. 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
Pogudin G., Scanlon T., Wibmer M., / Cornell University. Series "Working papers by Cornell University". 2019.
We study solutions of difference equations in the rings of sequences and, more generally, solutions of equations with a monoid action in the ring of sequences indexed by the monoid. This framework includes, for example, difference equations on grids (e.g., standard difference schemes) and difference equations in functions on words.
On the universality side, we prove ...
Added: November 1, 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, 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
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
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
Berlin : Springer, 2019
Edited in collaboration with FoLLI, the Association of Logic, Language and Information, this book constitutes the refereed proceedings of the 24th International Conference on Formal Grammar, FG 2019, held in Riga, Latvia, in August 2019, in conjunction with the 31st European Summer School in Logic, Language and Information, ESSLI 2019.
The 7 full papers presented were ...
Added: October 15, 2019
Lander Y., В кн. : Труды Международного семинара ДИАЛОГ'2001. Т. 1: Теоретические проблемы.: Аксаково : [б.и.], 2001. С. 151-158.
В статье обсуждается типология конструкций со счетными словами (нумеративами) и предлагается их формальное представление. ...
Added: May 1, 2014
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