?
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., 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., Journal of Logic and Computation 2021 Vol. 31 No. 5 P. 1266–1288
Изучается алгоритмическая выразительность предикатных логик шкалы Крипке, задаваемой множеством натуральных чисел с отношениями порядка. ...
Added: January 23, 2022
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
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
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., 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., 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
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
Pogudin G., Scanlon T., Wibmer M., / 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
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 definability in first-order predicate modal logic. On the one hand, it is wellknown that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e., a class of frames definable by a classical first-order formula, is recursively enumerable. On the ...
Added: October 25, 2019
Kanovich M., Kuznetsov S., Scedrov A., , in: Formal Grammar 2019, 24th International ConferenceVol. 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
Rybakov M., Shkatov D., , in: Theoretical Aspects of Computing – ICTAC 2018Vol. 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
Rybakov M., Shkatov D., , in: Proceedings of the South African Institute of Computer Scientists and Information Technologists 2019.: NY: ACM, 2019. Ch. 19 P. 1–7.
We present a simple proof of Thrakhtenbrot's theorem for the classical predicate logic in the language with only three individual variables. Both forms of Thrakhtenbrot's theorem are established: we prove that the classical predicate logic QCL over finite domains is not recursively enumerable in the language with only three individual variables and that the set ...
Added: October 6, 2019
Rybakov M., Shkatov D., , in: Proceedings of the Annual Conference of the South African Institute of Computer Scientists and Information Technologists.: NY: ACM, 2018. P. 313–316.
It is known that both satisfiability and model-checking problems for propositional Linear-time Temporal Logic, LTL, with only a single propositional variable in the language are PSPACE-complete, which coincides with the complexity of these problems for LTL with an arbitrary number of propositional variables. In the present paper, we show that the same result can be ...
Added: October 6, 2019