?
Horn fragments of the Halpern-Shoham interval temporal logic
P. 1–39.
Zakharyaschev M., BRESOLIN D., KURUCZ A., MUÑOZ-VELASCO E., RYZHIKOV V., SCIAVICCO G.
We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over dense orders under the irreflexive semantics but becomes undecidable over discrete orders under the irreflexive semantics. Satisfiability of binary Horn formulas with both boxes and diamonds is always undecidable under the irreflexive semantics.
Publication based on the results of:
Stepan L. Kuznetsov, , in: Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part II. (LNCS, volume 16689)Vol. 16689.: Cham: Springer, 2026. P. 161–177.
Kleene algebras are an algebraic abstraction of regular expressions, one of the central notions in computer science. While the equational theory of Kleene algebras is known to be decidable, reasoning from finite sets of hypotheses (Horn theory) quickly becomes undecidable. This happens even for simple classes of hypotheses which themselves do not involve Kleene star. ...
Added: July 26, 2026
Cham: Springer, 2025.
This book constitutes the refereed proceedings of the 21st Conference on Computability and Logic, CiE 2025, held in Lisbon, Portugal, during July 14–18, 2025.
The 27 full papers included in this book were carefully reviewed and selected from 49 submissions. They focus on computability-related science, ranging over mathematics, computer science and applications in various natural and engineering ...
Added: December 17, 2025
Kudinov A., Мясников К. М., Математика и теоретические компьютерные науки 2025 Т. 3 № 2 С. 58–84
The paper proves that for weakly transitive logics with the universal modality, whose formula satisfiability problem is in PSPACE, adding the connectedness axiom does not increase the complexity. Furthermore, an explicit algorithm solving this problem is presented. ...
Added: October 14, 2025
Blank M., Discrete and Continuous Dynamical Systems 2025 Vol. 45 No. 11 P. 4186–4201
Appeals to randomness in various number-theoretic constructions appear regularly in modern scientific publications. Such famous names as V.I. Arnold, M. Katz, Ya.G. Sinai, and T. Tao are just a few examples. Unfortunately, all of these approaches rely on various, although often very non-trivial and elegant, heuristics. A new analytical approach is proposed to address the ...
Added: May 23, 2025
Amirdjanov G. P., Gurevich I. B., Kostyuk F. V. et al., Pattern Recognition and Image Analysis 2023 Vol. 33 No. 4 P. 988–1049
The review presents the history of the creation and work of the Scientific Council “Cybernetics” (SCC)—the center for development of cybernetics in the USSR and Russia. The Council’s activity is covered as a structure that coordinates scientific and technical activity in cybernetics in the country via a system of sections: about 16 public and professional ...
Added: March 13, 2024
Смирнов И. А., Разумов П. В., Болдырихин Н. В. et al., IEEE, 2019.
Investigations of cryptographic algorithms for
today are very actually in connection with cybernetic attacks
threat and necessity of information protection at the
enterprises of various levels including the strategic
appointment. The project implementation of John Pollard’s
factorization ρ–method in the programming language C ++ is
presented, which works faster than the standard algorithm by
27%. It can facilitate greatly the deciphering operation ...
Added: May 10, 2023
Черкесова Л. В., Сафарьян О. А., Смирнов И. А., Молодой исследователь Дона 2018 Т. 3 (12) С. 111–121
The paper presents the project implementation of ρ-factor Pollard factorization in C ++, which works faster than the standard algorithm by 27%, which can significantly facilitate the work in deciphering and cryptanalysis of various ciphers such as RSA ...
Added: May 9, 2023
Stepan L. Kuznetsov, Journal of Logic and Computation 2023 Vol. 33 No. 6 P. 1437–1462
We prove undecidability and pinpoint the place in the arithmetical hierarchy for commutative action logic, i.e. the equational theory of commutative residuated Kleene lattices (action lattices), and infinitary commutative action logic, the equational theory of *-continuous commutative action lattices. Namely, we prove that the former is Σ01�10-complete and the latter is Π01�10-complete. Thus, the situation is the ...
Added: March 7, 2023
Popova E., Логико-философские штудии 2022 Vol. 20 No. 1 P. 1–7
There are two approaches to merging temporal and epistemic models. The first one consists in starting with a temporal model and enriching it with epistemic dimension (as temporal epistemic logic), while the second one is supposed to start with an epistemic model introducing temporal dimension (dynamic epistemic logic, epistemic temporal logic). The proposed evolutionary epistemic ...
Added: August 1, 2022
Faliszewski P., Karpov A., Obraztsova S., Autonomous Agents and Multi-Agent Systems 2022 Vol. 36 Article 18
We analyze the complexity of several NP-hard election-related problems under the assumptions that the voters have group-separable preferences. We show that under this assumption our problems typically remain NP-hard, but we provide more efficient algorithms if additionally the clone decomposition tree is of moderate height. We also show a polynomial-time algorithm for sampling group-separable elections uniformly at ...
Added: March 14, 2022
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785
Sequential reactive systems include programs and devices that work with two streams of
data and convert input streams of data into output streams. Such information processing systems
include controllers, device drivers, computer interpreters. The results of operation of such computing
systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite
transducers are most often ...
Added: January 17, 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
M.: [б.и.], 2021.
The Logical Perspectives Summer School and Workshop Series aims at giving advanced introductions into various branches of logic, and providing researchers — including early career scientists — with an opportunity to present their work.
In particular, LP 2021 Summer School (June 14–16) and Workshop (June 17–19) will focus on computational proof theory, broadly understood. The programme will comprise three ...
Added: December 14, 2021
Zakharyaschev M., Ryzhikov V., Wałęga P., Springer Publishing Company, 2020.
Added: November 8, 2021
Rybakov V., Siberian Mathematical Journal 2021 Vol. 62 P. 503–510
Under study are the branching time temporal logics with temporal accessibility relations for the agents different in length and content. We find an algorithm for solving the problems of satisfiability and decidability of the logic through describing finite satisfiable models of computable size (through the size of the input formulas). We remove the constraints on the ...
Added: November 8, 2021
Zakharyaschev M., Savateev Y., Ryzhikov V., Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2021.
Our concern is the problem of determining the data complexity of answering an ontology-mediated query (OMQ) given in linear temporal logic LTL over (Z, <) and deciding whether it is rewritable to an FO(<)-query, possibly with extra predicates. First, we observe that, in line with the circuit complexity and FO-definability of regular languages, OMQ answering ...
Added: November 6, 2021
Popova E., , in: Двенадцатые Смирновские чтения: материалы Международной научной конференции, Москва, 24–26 июня 2021 г.: М.: Русское общество истории и философии науки, 2021. P. 134–137.
This paper is concerned with the formalization problem of a wide range of scenarios of how knowledge evolves over time. We focus on combinations of temporal and epistemic modalities reflecting various properties of rational agents’ deliberation. For this purpose, we introduce the model EEM – evolutionary epistemic model. ...
Added: June 28, 2021
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
Gnatenko A., Zakharov V., Системная информатика 2020 Vol. 17 P. 21–32
Sequential reactive systems such as controllers, device drivers, computer interpreters operate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems of this kind. Since runs of transducers develop ...
Added: November 9, 2020
Kamenskikh A. A., В кн.: Логика и онтология в византийской догматической полемике. Очерки: Коллективная монографияТ. 19.: СПб.: Центр содействия образованию, 2020. С. 255–275.
The chapter of the collective monograph compares the temporal logics of late Neoplatonism and early Christian tradition; The problems of the genesis of the concept of time as a structure formed by a number of kairos moments, each of which may turn out to be a break point in the time series, are discussed. ...
Added: December 5, 2019
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences, Allerton Press Inc., United States 2019 Vol. 53 No. 7 P. 663–675
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a nite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between ows of control signals ...
Added: October 17, 2019