Jakub Rydval

Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability. One contribution of this paper is to strengthen the existing undecidability results further by showing that concrete domains even weaker than the ones considered in the previous proofs may cause undecidability. To regain decidability in the presence of GCIs, quite strong restrictions, in sum called omega-admissiblity, need to be imposed on the concrete domain. On the one hand, we generalize the notion of omega-admissiblity from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate omega-admissiblity to well-known notions from model theory. In particular, we show that finitely bounded, homogeneous structures yield omega-admissible concrete domains. This allows us to show omega-admissibility of concrete domains using existing results from model theory.

@inproceedings{ BaRy-IJCAR20,
  author = {Franz {Baader} and Jakub {Rydval}},
  booktitle = {Proceedings of the International Joint Conference on Automated Reasoning ({IJCAR} 2020)},
  editor = {Viorica {Sofronie-Stokkermans} and Nicolas {Peltier}},
  note = {To appear},
  title = {Description Logics with Concrete Domains and General Concept Inclusions Revisited},
  year = {2020},
}

Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability. One contribution of this paper is to strengthen the existing undecidability results further by showing that concrete domains even weaker than the ones considered in the previous proofs may cause undecidability. To regain decidability in the presence of GCIs, quite strong restrictions, in sum called omega-admissiblity, need to be imposed on the concrete domain. On the one hand, we generalize the notion of omega-admissiblity from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate omega-admissiblity to well-known notions from model theory. In particular, we show that finitely bounded, homogeneous structures yield omega-admissible concrete domains. This allows us to show omega-admissibility of concrete domains using existing results from model theory.

@techreport{ BaRy-LTCS-20-01,
  address = {Dresden, Germany},
  author = {Franz {Baader} and Jakub {Rydval}},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {20-01},
  title = {Using Model-Theory to Find $\omega$-Admissible Concrete Domains},
  type = {LTCS-Report},
  year = {2020},
}

Finite-domain constraint satisfaction problems are either solvable by Datalog, or not even expressible in fixed-point logic with counting. The border between the two regimes coincides with an important dichotomy in universal algebra; in particular, the border can be described by a strong height-one Maltsev condition. For infinite-domain CSPs the situation is more complicated even if the template structure of the CSP is model-theoretically tame. We prove that there is no Maltsev condition that characterises Datalog already for the CSPs of first-order reducts of (Q;<); such CSPs are called temporal CSPs and are of fundamental importance in infinite-domain constraint satisfaction. Our main result is a complete classification of temporal CSPs that can be solved in Datalog, and that can be solved in fixed point logic (with or without counting); the classification shows that many of the equivalent conditions in the finite fail to capture expressibility in any of these formalisms already for temporal CSPs.

@techreport{ BoPaRy-LTCS-20-04,
  address = {Dresden, Germany},
  author = {Manuel {Bodirsky} and Wied {Pakusa} and Jakub {Rydval}},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  number = {20-04},
  title = {Temporal Constraint Satisfaction Problems in Fixed-Point Logic},
  type = {LTCS-Report},
  year = {2020},
}