### ?

## Algorithmic properties of first-order modal logics of the natural number line in restricted languages

P. 523-539.

Rybakov M., Shkatov D.

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 with two individual variables and two monadic predicate letters. We also show that satisfiability for the logics is not arithmetical in languages with two individual variables, two monadic, and one 0-ary predicate letter.

Rybakov M., Shkatov D., Journal of Logic and Computation 2021 Vol. 31 No. 5 P. 1266-1288

Изучается алгоритмическая выразительность предикатных логик шкалы Крипке, задаваемой множеством натуральных чисел с отношениями порядка. ...

Added: January 23, 2022

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

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

Rybakov M., Shkatov D., , in : Advances in Modal Logic. Vol. 12.: College Publications, 2018. P. 531-539.

It is well-known that every quantied modal logic complete with respect to a first-order definable class of Kripke frames is recursively enumerable. Numerous examples are also known of natural quantied modal logics complete with respect to a class of frames dened by an essentially second-order condition which are not recursively enumerable. It is not, however, known if these ...

Added: October 6, 2019

Rybakov M., Shkatov D., Journal of Logic and Computation 2021 Vol. 31 No. 2 P. 426-443

It is shown that products and expanding relativized products of propositional modal logics where one component is the minimal monomodal logic K are polynomial-time reducible to their single-variable fragments. Therefore, the nown lower bound complexity and undecidability results for such logics are extended to their single-variable fragments. Similar results are obtained for products where one component is a polymodal logic with a K-style ...

Added: September 24, 2020

Rybakov M., Shkatov D., Theoretical Computer Science 2022 Vol. 925 P. 45-60

We prove that branching-time temporal logics CTL and CTL* are polynomial-time embeddable into their single-variable fragments. It follows that satisfiability for CTL and CTL*, and therefore also for alternating-time temporal logics ATL and ATL*, in languages with one propositional variable is as algorithmically hard as satisfiability for the full logic: EXPTIME-complete for CTL and ATL, and 2EXPTIME-complete for CTL* and ATL*. We discuss applicability of the technique used in the proofs to other ...

Added: May 12, 2022

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

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

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 satisﬁability problem. The complexity of satisﬁability for modal logics is rather high: it ranges from NP-complete to ...

Added: October 5, 2019

Rybakov M., Shkatov D., , in : Theoretical Aspects of Computing – ICTAC 2018. Vol. 11187.: Springer, 2018. P. 396-414.

We show that Branching-time temporal logics CTL and CTL*, as well as Alternating-time temporal logics ATL and ATL*, are as semantically expressive in the language with a single propositional variable as they are in the full language, i.e., with an unlimited supply of propositional variables. It follows that satisfiability for CTL, as well as for ATL, with a single variable is EXPTIME-complete, ...

Added: October 8, 2019

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

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., 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

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

Shkatov D., Rybakov M., , in : Conference of the South African Institute of Computer Scientists and Information Technologists 2020 (SAICSIT '20). : ACM, 2020. P. 58-65.

It is proved that Church theorem and Trakhtenbrot theorem are true for the logic of quasiary predicates. ...

Added: July 20, 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

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

Rybakov M., Shkatov D., Journal of Logic and Computation 2020 Vol. 30 No. 2 P. 549-560

We investigate the relationship between recursive enumerability and elementary frame deﬁnability in ﬁrst-order predicate modal logic. On the one hand, it is wellknown that every ﬁrst-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e., a class of frames deﬁnable by a classical ﬁrst-order formula, is recursively enumerable. On the ...

Added: October 25, 2019

Schloss Dagstuhl — Leibniz-Zentrum für Informatik, 2022

Added: September 26, 2022

Kanovich M., Kuznetsov S., Scedrov A., , in : Formal Grammar 2019, 24th International Conference. Vol. 11668.: Berlin : Springer, 2019. 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. ...

Added: October 15, 2019

Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356-371

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification ...

Added: January 17, 2022

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

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

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