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)},
  doi = {https://dx.doi.org/10.1007/978-3-030-51074-9\_24},
  editor = {Viorica {Sofronie-Stokkermans} and Nicolas {Peltier}},
  pages = {413--431},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Description Logics with Concrete Domains and General Concept Inclusions Revisited},
  volume = {12166},
  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.

@inproceedings{ BaRy-DL-20,
  address = {Online},
  author = {Franz {Baader} and Jakub {Rydval}},
  booktitle = {Proceedings of the 33rd International Workshop on Description Logics (DL'20)},
  editor = {Stefan {Borgwardt} and Thomas {Meyer}},
  publisher = {CEUR-WS},
  series = {CEUR Workshop Proceedings},
  title = {Description Logics with Concrete Domains and General Concept Inclusions Revisited (Extended Abstract)},
  volume = {2663},
  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 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 characterizes 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 expressed in one of the following logical formalisms: Datalog, fixed-point logic (with or without counting), or fixed-point logic with the Boolean rank operator. The classification shows that many of the equivalent conditions in the finite fail to capture expressibility in Datalog or fixed-point logic already for temporal CSPs.

@inproceedings{ BoRy-LICS20,
  address = {New York, NY, USA},
  author = {Manuel {Bodirsky} and Wied {Pakusa} and Jakub {Rydval}},
  booktitle = {Proceedings of the Symposium on Logic in Computer Science ({LICS} 2020)},
  doi = {https://dx.doi.org/10.1145/3373718.3394750},
  pages = {237--251},
  publisher = {Association for Computing Machinery},
  title = {Temporal Constraint Satisfaction Problems in Fixed-Point Logic},
  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},
}

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