Filter by type:

Sort by year

How to Tell Easy from Hard: Complexity of Conjunctive Query Entailment in Extensions of ALC

Bartosz Bednarczyk, Sebastian Rudolph
Journal Papers Journal of Artificial Intelligence Research (JAIR)

Abstract

It is commonly known that the conjunctive query entailment problem for certain ex- tensions of (the well-known ontology language) ALC is computationally harder than their knowledge base satisfiability problem while for others the complexities coincide, both under the standard and the finite-model semantics. We expose a uniform principle behind this divide by identifying a wide class of (finitely) locally-forward description logics, for which we prove that (finite) query entailment problem can be solved by a reduction to exponentially many calls of the (finite) knowledge base satisfiability problem. Consequently, our algorithm yields tight ExpTime upper bounds for locally-forward logics with ExpTime-complete knowledge base satisfiability problem, including logics between ALC and μALCHbregQ (and more), as well as ALCSCC with global cardinality constraints, for which the complexity of querying remained open. Moreover, to make our technique applicable in future research, we provide easy-to-check sufficient conditions for a logic to be locally-forward based on several novel versions of the model-theoretic notion of unravellings. Together with existing results, this provides a nearly complete classification of the “benign” vs. “malign” primitive modelling features extending ALC, missing out only the Self operator. We then show a rather surprising result, namely that the conjunctive entailment problem for ALCSelf is exponentially harder than for ALC. This places the seemingly innocuous Self operator among the “malign” modelling features, like inverses, transitivity or nominals.

Beyond ALCreg: Exploring Non-Regular Extensions of PDL with Description Logics Features

Bartosz Bednarczyk
Conference Papers Proceedings of the 18th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2023)

Abstract

We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics. Our primary object of interest is ALCvpl, an extension of ALC with path expressions using visibly-pushdown languages, which was shown to be decidable by Löding et al. in 2007. The paper present a series of undecidability results. We prove undecidability of ALCvpl with the seemingly innocent Self operator. Then, we consider the simplest non-regular (visibly-pushdown) language r#s# := {rnsn | n ∈ N}. We establish un- decidability of the concept satisfiability problem for ALCreg extended with nominals and r#s#, as well as of the query entailment problem for ALC-TBoxes, where such non-regular atoms are present in queries.

On the Limits of Decision: the Adjacent Fragment of First-Order Logic

Bartosz Bednarczyk, Daumantas Kojelis and Ian Pratt-Hartmann
Conference Papers Proceedings of the 50th EATCS International Colloquium on Automata, Languages and Programming (ICALP 2023)

Abstract

We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.

On Composing Finite Forests with Modal Logics

Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti
Journal Papers ACM Transactions on Computational Logic

Abstract

We study the expressivity and complexity of two modal logics interpreted on inite forests and equipped with standard modalities to reason on submodels. The logic ML( ) extends the modal logic K with the composition operator from ambient logic, whereas ML(∗) features the separating conjunction ∗ from separation logic. Both operators are second-order in nature. We show that ML( ) is as expressive as the graded modal logic GML (on trees) whereas ML(∗) is strictly less expressive than GML. Moreover, we establish that the satisfiability problem is Tower-complete for ML(∗), whereas it is (only) AExpPolcomplete for ML( ), a result which is surprising given their relative expressivity. As by-products, we solve open problems related to sister logics such as static ambient logic and modal separation logic.

Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

Bartosz Bednarczyk, Stéphane Demri
Journal Papers Logical Methods in Computer Science

Abstract

Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that tQCTL restricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When tQCTL restricted to EX is interpreted on N-bounded trees for some N >= 2, we prove that the satisfiability problem is AExpPol-complete; AExpPol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As consequences of our proof method, we prove Tower-hardness of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as K, KD, GL, K4 and S4 with propositional quantification under a semantics based on classes of trees.

Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting

Bartosz Bednarczyk, Oskar Fiuk
Conference Papers Proceedings of the 28th Workshop on Logic, Language, Information and Computation (WOLLIC 2022)

Abstract

We introduce two versions of Presburger Automata with the Büchi acceptance condition, working over infinite, finite-branching trees. These automata, in addition to the classical ones, allow nodes for checking linear inequalities over labels of their children. We establish tight NP and ExpTime bounds on the complexity of the non-emptiness problem for the presented machines. We demonstrate the usefulness of our automata models by polynomially encoding the two-variable guarded fragment extended with Presburger constraints, improving the existing triply-exponential upper bound to a single exponential.

Towards Model Theory of Ordered Logics: Expressivity and Interpolation

Bartosz Bednarczyk, Reijo Jaakkola
Conference Papers Proceedings of the 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract

We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it. We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the relative expressive power of ordered logics, and to characterise our logics as bisimulation-invariant fragments of FO à la van Benthem. Afterwards, we study the Craig Interpolation Property (CIP). We refute yet another claim from the infamous work by Purdy, by showing that the fluted and forward fragments do not enjoy CIP. We complement this result by showing that the ordered fragment and the guarded ordered logics enjoy CIP. These positive results rely on novel and quite intricate model constructions, which take full advantage of the ``forwardness'' of our logics.

Comonadic Semantics for Description Logics Games

Bartosz Bednarczyk, Mateusz Urbańczyk
Workshop Papers Proceedings of the Description Logics Workshop 2022

Abstract

A categorical approach to study model comparison games in terms of comonads was recently initiated by Abramsky et al. In this work, we analyse games that appear naturally in the context of description logics and supplement them with suitable game comonads. More precisely, we consider expressive sublogics of ALCSelf IbO, namely, the logics that extend ALC with any combination of inverses, nominals, safe boolean roles combinations and the Self operator. Our construction augments and modifies the so-called modal comonad by Abramsky and Shah. The approach that we took heavily relies on the use of relative monads, which we leverage to encapsulate additional capabilities within the bisimulation games in a compositional manner.

Finite Entailment of Local Queries in the Z Family of Description Logics

Bartosz Bednarczyk, Emanuel Kieroński
Conference Papers Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI 2022)

Abstract

In the last few years the field of logic-based knowledge representation took a lot of inspiration from database theory. A vital example is that the finite model semantics in description logics (DLs) is reconsidered as a desirable alternative to the classical one and that query entailment has replaced knowledge-base satisfiability (KBSat) checking as the key inference problem. However, despite the considerable effort, the overall picture concerning finite query answering in DLs is still incomplete. In this work we study the complexity of finite entailment of local queries (conjunctive queries and positive boolean combinations thereof) in the Z family of DLs, one of the most powerful KR formalisms, lying on the verge of decidability. Our main result is that the DLs ZOQ and ZOI are finitely controllable, i.e. that their finite and unrestricted entailment problems for local queries coincide. This allows us to reuse recently established upper bounds on querying these logics under the classical semantics. While we will not solve finite query entailment for the third main logic in the Z family, ZIQ, we provide a generic reduction from the finite entailment problem to the finite KBSat problem, working for ZIQ and some of its sublogics. Our proofs unify and solidify previously established results on finite satisfiability and finite query entailment for many known DLs.

The Price of Selfishness: Conjunctive Query Entailment for ALCSelf is 2EXPTIME-Hard

Bartosz Bednarczyk, Sebastian Rudolph
Conference Papers Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI 2022)

Abstract

Abstract: In logic-based knowledge representation, query answering has essentially replaced mere satisfiability checking as the inferencing problem of primary interest. For knowledge bases in the basic description logic ALC, the computational complexity of conjunctive query (CQ) answering is well known to be EXPTIME-complete and hence not harder than satisfiability. This does not change when the logic is extended by certain features (such as counting or role hierarchies), whereas adding others (inverses, nominals or transitivity together with role-hierarchies) turns CQ answering exponentially harder. We contribute to this line of results by showing the surprising fact that even extending ALC by just the Self operator – which proved innocuous in many other contexts – increases the complexity of CQ entailment to 2EXPTIME. As common for this type of problem, our proof establishes a reduction from alternating Turing machines running in exponential space, but several novel ideas and encoding tricks are required to make the approach work in that specific, restricted setting.

On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics

Bartosz Bednarczyk, Maja Orłowska, Anna Pacanowska, Tony Tan
Conference Papers Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract

During the last decades, a lot of effort was put into identifying decidable fragments of first-order logic. Such efforts gave birth, among the others, to the two-variable fragment and the guarded fragment, depending on the type of restriction imposed on formulae from the language. Despite the success of the mentioned logics in areas like formal verification and knowledge representation, such first-order fragments are too weak to express even the simplest statistical constraints, required for modelling of influence networks or in statistical reasoning. In this work we investigate the extensions of these classical decidable logics with percentage quantifiers, specifying how frequently a formula is satisfied in the indented model. We show, surprisingly, that all the mentioned decidable fragments become undecidable under such extension, sharpening the existing results in the literature. Our negative results are supplemented by decidability of the two-variable guarded fragment with even more expressive counting, namely Presburger constraints. Our results can be applied to infer decidability of various modal and description logics, e.g. Presburger Modal Logics with Converse or ALCI, with expressive cardinality constraints.

The Price of Selfishness: Conjunctive Query Entailment for ALCSelf is 2ExpTime-hard (Extended Abstract)

Bartosz Bednarczyk, Sebastian Rudolph
Workshop Papers Proceedings of the Description Logics Workshop 2021

Finite-Controllability of Conjunctive Queries in the Z family of Description Logics (Extended Abstract)

Bartosz Bednarczyk, Emanuel Kieroński
Workshop Papers Proceedings of the Description Logics Workshop 2021

Completing the Picture: Complexity of Graded Modal Logics with Converse

Bartosz Bednarczyk, Emanuel Kieroński, Piotr Witkowski
Journal Papers Theory and Practice of Logic Programming

Abstract

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames have already been established. By ”traditional” classes of frames, we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper, we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular, we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

Statistical EL is ExpTime-complete

Bartosz Bednarczyk
Journal Papers Information Processing Letters

Abstract

We show that the consistency problem for Statistical EL ontologies, defined by Penaloza and Potyka in SUM 2017, is ExpTime-hard. Together with existing ExpTime upper bounds, we conclude ExpTime-completeness of the logic. Our proof goes via a reduction from the consistency problem for EL extended with negation of atomic concepts.

Exploiting forwardness: Satisfiability and Query-Entailment in Forward Guarded Fragment

Bartosz Bednarczyk
Conference Papers [Best student paper award] Proceedings of the 17th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2021)

Abstract

We study the complexity of two standard reasoning problems for Forward Guarded Logic (FGF), obtained as a restriction of the Guarded Fragment in which variables appear in atoms only in the order of their quantification. We show that FGF enjoys the higher-arity-forest- model property, which results in ExpTime-completeness of its (finite and unrestricted) knowledge-base satisfiability problem. Moreover, we show that FGF is well-suited for knowledge representation. By employing a generalisation of Lutz’s spoiler technique, we prove that the conjunctive query entailment problem for FGF remains in ExpTime. We find that our results are quite unusual as FGF is, up to our knowledge, the first decidable fragment of First-Order Logic, extending standard description logics like ALC, that offers unboundedly many variables and higher-arity relations while keeping its complexity surprisingly low.

"Most of" leads to undecidability: Failure of adding frequencies to LTL

Bartosz Bednarczyk, Jakub Michaliszyn
Conference Papers Proceedings of the 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021).

Abstract

Linear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that sigma is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and briefly discuss how the undecidability results transfer to first-order logic on words.

A note on C2 interpreted over finite data-words

Bartosz Bednarczyk, Piotr Witkowski
Conference Papers Proceedings of the 27th International Symposium on Temporal Representation and Reasoning (TIME 2020).

Abstract

We consider the satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers, interpreted over finite words with data, denoted here with C2[≤,succ,∼,πbin]. In our scenario, we allow for using arbitrary many uninterpreted binary predicates from ,πbin, two navigational predicates ≤ and succ over word positions as well as a data-equality predicate ~. We prove that the obtained logic is undecidable, which contrasts with the decidability of the logic without counting by Montanari, Pazzaglia and Sala [MontanariPS16]. We supplement our results with decidability for several sub-fragments of C2[≤,succ,∼,πbin], e.g., without binary predicates, without successor succ, or under the assumption that the total number of positions carrying the same data value in a data-word is bounded by an a priori given constant.

All-Instances Oblivious Chase Termination is Undecidable for Single-Head Binary TGDs

Bartosz Bednarczyk, Robert Ferens, Piotr Ostropolski-Nalewaja
Conference Papers Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI 2020).

Abstract

The chase is a famous algorithmic procedure in database theory with numerous applications in ontology-mediated query answering. We consider static analysis of the chase termination problem, which asks, given set of TGDs, whether the chase terminates on all input databases. The problem was recently shown to be undecidable by Gogacz et al. for sets of rules containing only ternary predicates. In this work, we show that undecidability occurs already for sets of single-head TGD over binary vocabularies. This question is relevant since many real-world ontologies, e.g., those from the Horn fragment of the popular OWL, are of this shape.

A Framework for Reasoning about Dynamic Axioms in Description Logics

Bartosz Bednarczyk, Stephane Demri, Alessio Mansutti
Conference Papers Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI 2020).

Abstract

Description logics are well-known logical formalisms for knowledge representation. We propose to enrich knowledge bases (KBs) with dynamic axioms that specify how the satisfaction of statements from the KBs evolves when the interpretation is decomposed or recomposed, providing a natural means to predict the evolution of interpretations. Our dynamic axioms borrow logical connectives from separation logics, well-known specification languages to verify programs with dynamic data structures. In the paper, we focus on ALC and EL augmented with dynamic axioms, or to their subclass of positive dynamic axioms. The knowledge base consistency problem in the presence of dynamic axioms is investigated, leading to interesting complexity results, among which the problem for EL with positive dynamic axioms is tractable, whereas EL with dynamic axioms is undecidable.

Modal Logics with Composition on Finite Forests: Expressivity and Complexity

Bartosz Bednarczyk, Stephane Demri, Raul Fervari, Alessio Mansutti
Conference Papers Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020

Abstract

We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(∗) contains the separating conjunction ∗ from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(∗) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(∗) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete.As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.s

Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints

Franz Baader, Bartosz Bednarczyk, Sebastian Rudolph
Conference Papers Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020).

Abstract

Abstract. We introduce and investigate the expressive description logic (DL) ALCSCC++, in which the global and local cardinality constraints introduced in previous papers can be mixed. We prove that the added expressivity does not increase the complexity of satisfiability checking and other standard inference problems. However, reasoning in ALCSCC++ becomes undecidable if inverse roles are added or conjunctive query entailment is considered. We prove that decidability of querying can be regained if global and local constraints are not mixed and the global constraints are appropriately restricted. In this setting, query entailment can be shown to be EXPTIME-complete and hence not harder than reasoning in ALC.

One-Variable Logic Meets Presburger Arithmetic

Bartosz Bednarczyk
Journal Papers Theoretical Computer Science

Abstract

We consider the one-variable fragment of first-order logic extended with Presburger constraints. The logic is designed in such a way that it subsumes the previously-known fragments extended with counting, modulo counting or cardinality comparison and combines their expressive powers. We prove NP-completeness of the logic by presenting an optimal algorithm for solving its finite satisfiability problem.

Worst-Case Optimal Querying of Very Expressive Description Logics with Path Expressions and Succinct Counting

Bartosz Bednarczyk, Sebastian Rudolph
Conference Papers Proceedings of the 28th International Joint Conference on Artificial Intelligence, IJCAI 2019

Abstract

Among the most expressive knowledge representation formalisms are the description logics of the Z family. For well-behaved fragments of ZOIQ, entailment of positive two-way regular path queries is well known to be 2EXPTIMEcomplete under the proviso of unary encoding of numbers in cardinality constraints. We show that this assumption can be dropped without an increase in complexity and EXPTIME-completeness can be achieved when bounding the number of query atoms, using a novel reduction from query entailment to knowledge base satisfiability. These findings allow to strengthen other results regarding query entailment and query containment problems in very expressive description logics. Our results also carry over to GC2 , the two-variable guarded fragment of firstorder logic with counting quantifiers, for which hitherto only conjunctive query entailment has been investigated.

Worst-Case Optimal Querying of Very Expressive Description Logics with Path Expressions and Succinct Counting

Bartosz Bednarczyk, Sebastian Rudolph
Workshop Papers Proceedings of the Description Logics Workshop 2019

Abstract

Among the most expressive knowledge representation formalisms are the description logics of the Z family. For well-behaved fragments of ZOIQ, entailment of positive two-way regular path queries is well known to be 2EXPTIMEcomplete under the proviso of unary encoding of numbers in cardinality constraints. We show that this assumption can be dropped without an increase in complexity and EXPTIME-completeness can be achieved when bounding the number of query atoms, using a novel reduction from query entailment to knowledge base satisfiability. These findings allow to strengthen other results regarding query entailment and query containment problems in very expressive description logics. Our results also carry over to GC2 , the two-variable guarded fragment of firstorder logic with counting quantifiers, for which hitherto only conjunctive query entailment has been investigated.

Satisfiability Checking and Conjunctive Query Answering in Description Logics with Global and Local Cardinality Constraints

Franz Baader, Bartosz Bednarczyk, Sebastian Rudolph
Workshop Papers Proceedings of the Description Logics Workshop 2019

Abstract

We consider an expressive description logic (DL) in which the global and local cardinality constraints introduced in previous papers can be mixed. On the one hand, we show that this does not increase the complexity of satisfiability checking and other standard inference problems. On the other hand, conjunctive query entailment in this DL turns out to be undecidable. We prove that decidability of querying can be regained if global and local constraints are not mixed and the global constraints are appropriately restricted.

Why propositional quantification makes modal logics on trees robustly hard ?

Bartosz Bednarczyk, Stephane Demri
Conference Papers Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019

Abstract

Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability whereas CTL with propositional quantification under the tree semantics (written QCTLt) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of QCTLt as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that QCTLt restricted to the temporal operator EX is already Tower-hard, which is unexpected as, for instance, EX can only enforce local properties. When QCTLt restricted to EX is interpreted on N-bounded trees for some N >= 2, we prove that the satisfiability problem is AExppol-complete; AExppol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As significant consequences of our proof method, we prove Tower-hardness of QCTLt restricted to EF or to EXEF and of the well-known modal logics K, KD, GL, S4, K4 and D4, with propositional quantification under a semantics based on classes of trees.

On the Complexity of Graded Modal Logics with Converse

Bartosz Bednarczyk, Emanuel Kieroński, Piotr Witkowski
Conference Papers Proceedings of the 16th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2019)

Abstract

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames has already been established. By 'traditional' classes of frames we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

Modulo Counting on Words and Trees

Bartosz Bednarczyk, Witold Charatonik
Conference Papers Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11–15, 2017, Kanpur, India. LIPIcs 93, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2017, pages 12:1–12:16.

Abstract

We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.

Extending Two-Variable Logic on Trees

Bartosz Bednarczyk, Witold Charatonik, Emanuel Kieroński
Conference Papers Proceedings of the 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden. LIPIcs 82, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2017, pages 11:1-11:20

Abstract

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

On One Variable Fragment of First Order Logic with Modulo Counting Quantifier

Bartosz Bednarczyk
Conference Papers Proceedings of ESSLLI 2017 Student Session, 29th European Summer School in Logic, Language & Information, July 17-28, 2017, Toulouse, France, pages 7-13

Abstract

We consider the one-variable fragment of first-order logic extended with modulo counting quantifiers. We prove NPTime-completeness of such fragment by presenting an optimal algorithm for solving its finite satisfiability problem.

Satisfiability of the Two-Variable Fragment of First-Order Logic with counting quantifiers over finite trees

Bartosz Bednarczyk
Bachelor Thesis Dissertation advisor: prof. dr hab. Witold Charatonik, Date of defence: Feb. 15, 2017

Abstract

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We show that adding counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem.