A Tableau Algorithm for DLs with Concrete Domains and GCIs
Institut für Theoretische Informatik TU Dresden, Carsten Lutz, Maja Miličić, Institut für Theoretische Informatik TU Dresden · 2005
We identify a general property of concrete domains that is sufficient for proving decidability of DLs equipped with them and GCIs. We show that some useful concrete domains, such as temporal one based on the Allen relations and a spatial one based on the RCC-8 relations, have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with such concrete domains.