Searcharxiv⌕ Search

arXiv subjects

Dmitry Shkatov

Publications and source records attributed to Dmitry Shkatov.

15 recordsLinked to original sources
arXiv2026

Some prospects for semiproducts and products of modal logics

We consider products and semiproducts of propositional modal logics L with S5 and present new examples of product and semiproduct logics axiomatized in the minimal way and enjoying the product (or semiproduct) FMP. An essential part of the proof is local tabularity of these (semi)products for L of finite depth; it is obtained by using bisimulation games. These results readily imply decidability for 1-variable fragments of predicate modal logics QL and QL+Barcan formula. We also present new counterexamples, i.e. (semi)products not axiomatizable in the simplest way.

math.LO↗
arXiv2026

Fusions of One-Variable First-Order Modal Logics

We investigate preservation results for the independent fusion of one-variable first-order modal logics. We show that, without equality, Kripke completeness and decidability of global and local consequence relations are preserved, under both expanding and constant domain semantics. By contrast, Kripke completeness and decidability are not preserved for fusions with equality and non-rigid constants (or, equivalently, counting up to one), again for the global and local consequence and under both expanding and constant domain semantics. This result is shown by encoding Diophantine equations. Even without equality, the finite model property is preserved only in the local case. Finally, we view fusions of one-variable modal logics as fusions of propositional modal logics sharing an S5 modality and provide a general sufficient condition for transfer of Kripke completeness and decidability (but not of finite model property).

cs.LO↗
arXiv2022

Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter

We prove that the positive fragment of first-order intuitionistic logic in the language with two variables and a single monadic predicate letter, without 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 is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser's basic and formal logics, respectively. We also show that, for most "natural" first-order modal logics, the two-variable fragment with a single monadic predicate letter, without constants and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz -- among them, QK, QT, QKB, QD, QK4, and QS4.

cs.LO↗
arXiv2021

Algorithmic properties of first-order modal logics of linear Kripke frames in restricted languages

We study the algorithmic properties of first-order monomodal logics of frames $\langle \mathbb{N}, \leq \rangle$, $\langle \mathbb{N}, < \rangle$, $\langle \mathbb{Q}, \leq \rangle$, $\langle \mathbb{Q}, < \rangle$, $\langle \mathbb{R}, \leq \rangle$, $\langle \mathbb{R}, < \rangle$, as well as some related logics, in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We show that the logics of frames based on $\mathbb{N}$ are $Π^1_1$-hard -- thus, not recursively enumerable -- in languages with two individual variables, one monadic predicate letter and one proposition letter. We also show that the logics of frames based on $\mathbb{Q}$ and $\mathbb{R}$ are $Σ^0_1$-hard in languages with the same restrictions. Similar results are obtained for a number of related logics.

cs.LO↗
arXiv2019

Recursive enumerability and elementary frame definability in predicate modal logic

We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On the one hand, it is well-known 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 other, numerous examples are known of predicate modal logics, based on `natural' propositional modal logics with essentially second-order Kripke semantics, that are either not recursively enumerable or Kripke incomplete. This raises the question of whether every Kripke complete, recursively enumerable predicate modal logic can be characterized by an elementary class of Kripke frames. We answer this question in the negative, by constructing a normal predicate modal logic which is Kripke complete, recursively enumerable, but not complete with respect to an elementary class of frames. We also present an example of a normal predicate modal logic that is recursively enumerable, Kripke complete, and not complete with respect to an elementary class of rooted frames, but is complete with respect to an elementary class of frames that are not rooted.

math.LO↗
arXiv2019

Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time

We develop a tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of linear time CMATEL(CD+LT). It extends LTL with operators of common and distributed knowledge for all coalitions of agents. The tableau procedure runs in exponential time, matching the lower bound obtained by Halpern and Vardi for a fragment of our logic, thus providing a complexity-optimal decision procedure for CMATEL(CD+LT).

cs.LO↗
arXiv2019

Complexity of finite-variable fragments of propositional modal logics of symmetric frames

While finite-variable fragments of the propositional modal logic S5--complete with respect to reflexive, symmetric and transitive frames--are polynomial-time decidable, the restriction to finite-variable formulas for logics of reflexive and transitive frames yields fragments that remain "intractable." The role of the symmetry condition in this context has not been investigated. We show that symmetry either by itself or in combination with reflexivity produces logics that behave just like logics of reflexive and transitive frames, i.e. their finite-variable fragments remain intractable, namely PSPACE-hard. This raises the question of where exactly the borderline lies between modal logics whose finite-variable fragments are tractable and the rest.

math.LO↗
arXiv2019

Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables

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, while satisfiability for CTL*, as well as for ATL*, with a single variable is 2EXPTIME-complete,--i.e., for these logics, the satisfiability for formulas with only one variable is as hard as satisfiability for arbitrary formulas.

cs.LO↗
arXiv2019

Complexity and expressivity of propositional dynamic logics with finitely many variables

We investigate the complexity of satisfiability for finite-variable fragments of propositional dynamic logics. We consider three formalisms belonging to three representative complexity classes, broadly understood,---regular PDL, which is EXPTIME-complete, PDL with intersection, which is 2EXPTIME-complete, and PDL with parallel composition, which is undecidable. We show that, for each of these logics, the complexity of satisfiability remains unchanged even if we only allow as inputs formulas built solely out of propositional constants, i.e. without propositional variables. Moreover, we show that this is a consequence of the richness of the expressive power of variable-free fragments: for all the logics we consider, such fragments are as semantically expressive as entire logics. We conjecture that this is representative of PDL-style, as well as closely related, logics.

cs.LO↗
arXiv2018

On complexity of propositional Linear-time Temporal Logic with finitely many variables

It is known [DemriSchnoebelen02] 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 [SislaClarke85]. In the present paper, we show that the same result can be obtained by modifying the original proof of SPACE-hardness for LTL from [SislaClarke85]; i.e., we show how to modify the construction from [SislaClarke85] to model the computations of polynomially-space bound Turing machines using only formulas of one variable. We believe that our alternative proof of the results from [DemriSchnoebelen02] gives additional insight into the semantic and computational properties of LTL.

cs.LO↗
arXiv2012

Tableau-based decision procedure for the multi-agent epistemic logic with all coalitional operators for common and distributed knowledge

We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi-agent epistemic logic CMAEL(CD) with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for CMAEL(CD) and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable input set of formulae of CMAEL(CD) and closes for every unsatisfiable input set of formulae.

cs.LO↗
arXiv2009

Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic

We study the multiagent epistemic logic CMAELCD with operators for common and distributed knowledge for all coalitions of agents. We introduce Hintikka structures for this logic and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using this result, we design an incremental tableau based decision procedure for testing satisfiability in CMAELCD.

cs.LO↗
arXiv2008

Tableau-based decision procedures for logics of strategic ability in multi-agent systems

We develop an incremental tableau-based decision procedures for the Alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we claim that our tableau is practically more efficient in the average case than other decision procedures for ATL known so far. Besides, the ease of its adaptation to variants of ATL demonstrates the flexibility of the proposed procedure.

cs.LO↗
arXiv2008

Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge

We develop an incremental-tableau-based decision procedure for the multi-agent epistemic logic MAEL(CD) (aka S5_n (CD)), whose language contains operators of individual knowledge for a finite set Ag of agents, as well as operators of distributed and common knowledge among all agents in Ag. Our tableau procedure works in (deterministic) exponential time, thus establishing an upper bound for MAEL(CD)-satisfiability that matches the (implicit) lower-bound known from earlier results, which implies ExpTime-completeness of MAEL(CD)-satisfiability. Therefore, our procedure provides a complexity-optimal algorithm for checking MAEL(CD)-satisfiability, which, however, in most cases is much more efficient. We prove soundness and completeness of the procedure, and illustrate it with an example.

cs.LO↗