DESCRIPTION LOGICS WITH CONCRETE DOMAINS
========================================

Definition:

A set of objects D, distinct from the set of abstract symbols, is a
concrete domain if (a) it is organized into a type system; and (b) it
is equipped with an operator that decides if two datatypes intersect.
(This also gives membership checking, as the intersection between a
signgleton and a datatype.)

Alternative definition you might come across:

The pair <D,Phi> is a concrete domain if D is a set of objects
distinct from the set of abstract symbols and Phi is a set of n-ary
predicates over D such that (a) there is a top, i.e., a predicate that
is true for all of D; (b) negation is closed with respect to D; and
(c) satisfiability of finite conjuctions of predicates from Phi is
decidable.


The domain can be anything with these properties: numerical,
spatiotemporal, FSAs over strings.

For example, for integers N:

[0..] is a subtype of N
[3..5] subtype of [0..]
[4..10] subtype of [0..]
[-2..2] subtype of N

Note how subtypes are not necessarily a partitioning.

Using the alternative definition these subtypes would be conjunctions
of the familiar 2-ary predicates less-then, greater-than,
less-or-equal, etc. The solver is the familiar algorithm for solving
systems of linear inequalities.  



NEW CONSTRUCTS
==============

As usually, I() interpets a class as a set of abstract object and a
property (aka a role) as a set of pairs of abstract objects.

New operator D() interpets datatypes as sets of items from the the
concrete domain.

These constructs can be used to define concepts (sets of abstract
objects) based on the fillers of concrete properties:

\exists T.d means: { x | \exists y. <x,y> \in I(T) and y \in D(d) }
\forall T.d means: { x | \forall y. <x,y> \in I(T) implies y \in D(d) }
 
example datatype:
RetirementAge = {n \in N^+ | n > 67}

example concept:
Retired \subset Person \and \forall age.RetirementAge



PROOF THEORY
============

Tableaux as we know it, with extra clash conditions:

L() maps individuals to class descriptions.
E() maps concrete attributes to <individual,value> pairs

Branch expansion rules:

forall T.d in L(s)
<s,v> in E(T)
---------------
v in D(d)

exists T.d in L(s)
---------------
exists <s,v> : <s,v> in E(T) and v in D(d) 

In the syntax we are more familiar with in DLs,
where s:C is used to express that s is a member of C:

s : (forall T.d)
<s,v> : T
---------------
v in D(d)

s : (exists T.d)
---------------
exists v such that <s,v>:T and v in D(d) 

Carefull: only v is a fresh (skolem) symbol, s is the object that is
in the concept (exists T.d). The existential refers to the concrete
filler, not s.