25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Schloss Dagstuhl — Leibniz-Zentrum für Informatik, 2022.
Under the general editorship: K. Meel, O. Strichman
, , , , in : 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). : Schloss Dagstuhl — Leibniz-Zentrum für Informatik, 2022.
We show that for any connected graph G the size of any regular resolution or OBDD(∧, reordering) refutation of a Tseitin formula based on G is at least 2^Ω(tw(G)), where tw(G) is the treewidth of G. These lower bounds improve upon the previously known bounds and, moreover, they are tight. For both of the proof systems, ...
Added: September 26, 2022
, , 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
Complexity and expressivity of Branching- and Alternating-time temporal logics with finitely many variables
, , , 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
, , , 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
О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени
, , Моделирование и анализ информационных систем 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
, , 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
, , 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
Algorithmic properties of first-order modal logics of the natural number line in restricted languages
, , , 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