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},
}

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},
}