Filippo De Bortoli

In recent work we have extended the description logic (DL) by means of more expressive number restrictions using numerical and set constraints stated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA). It has been shown that reasoning in the resulting DL, called \(\mathcal{ALCSCC}\), is PSpace-complete without a TBox and ExpTime-complete w.r.t. a general TBox. The semantics of \(\mathcal{ALCSCC}\) is defined in terms of finitely branching interpretations, that is, interpretations where every element has only finitely many role successors. This condition was needed since QFBAPA considers only finite sets. In this paper, we first introduce a variant of \(\mathcal{ALCSCC}\), called \(\mathcal{ALCSCC}^\infty\), in which we lift this requirement (inexpressible in first-order logic) and show that the complexity results for \(\mathcal{ALCSCC}\) mentioned above are preserved. Nevertheless, like \(\mathcal{ALCSCC}\), \(\mathcal{ALCSCC}^\infty\) is not a fragment of first-order logic. The main contribution of this paper is to give a characterization of the first-order fragment of \(\mathcal{ALCSCC}^\infty\). The most important tool used in the proof of this result is a notion of bisimulation that characterizes this fragment.

@inproceedings{ BaDeBo-FroCoS19,
  author = {Franz {Baader} and Filippo {De Bortoli}},
  booktitle = {Proc. of the 12th International Symposium on Frontiers of Combining Systems ({FroCoS} 2019)},
  doi = {https://doi.org/10.1007/978-3-030-29007-8_12},
  editor = {Andreas {Herzig} and Andrei {Popescu}},
  pages = {203--219},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {On the Expressive Power of Description Logics with Cardinality Constraints on Finite and Infinite Sets},
  volume = {11715},
  year = {2019},
}

Simple counting quantifiers that can be used to compare the number of role successors of an individual or the cardinality of a concept with a fixed natural number have been employed in Description Logics (DLs) for more than two decades under the respective names of number restrictions and cardinality restriction on concepts. Recently, we have considerably extended the expressivity of such quantifiers by allowing to impose set and cardinality constraints formulated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA) on sets of role successors and concepts, respectively. We were able to prove that this extension does not increase the complexity of reasoning. In the present paper, we investigate the expressive power of the DLs obtained this way, using appropriate bisimulation characterizations and 0–1 laws as tools for distinguishing the expressiveness of different logics. In particular, we show that, in contrast to most classical DLs, these logics are no longer expressible in first-order predicate logic (FOL), and we characterize their first-order fragments. In most of our previous work on DLs with QFBAPA-based set and cardinality constraints we have employed finiteness restrictions on interpretations to ensure that the obtained sets are finite. Here we dispense with these restrictions to make the comparison with classical DLs, where one usually considers arbitrary models rather than finite ones, easier. It turns out that doing so does not change the complexity of reasoning.

@techreport{ BaBo-LTCS-19-09,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Filippo {De Bortoli}},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {\url{https://tu-dresden.de/inf/lat/reports#BaBo-LTCS-19-09}},
  number = {19-09},
  title = {{On the Complexity and Expressiveness of Description Logics with Counting}},
  type = {LTCS-Report},
  year = {2019},
}

Recent research in the field of Description Logic (DL) investigated the complexity of the satisfiability problem for description logics that are obtained by enriching the well-known DL with more complex set and cardinality constraints over role successors. The algorithms that have been proposed so far, despite providing worst-case optimal decision procedures for the concept satisfiability problem (both without and with a terminology) lack the efficiency needed to obtain usable implementations. In particular, the algorithm for the case without terminology is non-deterministic and the one for the case with a terminology is also best-case exponential. The goal of this thesis is to use well-established techniques from the field of numerical optimization, such as column generation, in order to obtain more practical algorithms. As a starting point, efficient approaches for dealing with counting quantifiers over unary predicates based on SAT-based column generation should be considered.

@thesis{ DeBo-Mas-19,
  address = {Dresden, Germany},
  author = {Filippo {De Bortoli}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Integrating Reasoning Services for Description Logics with Cardinality Constraints with Numerical Optimization Techniques},
  type = {Master's Thesis},
  year = {2019},
}