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  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.  \in I(T) and y \in D(d) }
\forall T.d means: { x | \forall 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  pairs

Branch expansion rules:

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

exists T.d in L(s)
---------------
exists  :  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)
 : T
---------------
v in D(d)

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

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




MANY-VALUED LOGICS
==================

Mmany-valued membership functions map concrete values (such as
height, weight) to a membership degree in [0..1]. Any function
will do as long as it captures the domain well. Usually there will a
flat part at the edges of the value's domain for the region where the
value definitely is or is not in the intended concept; and a straight
or sigmoid function that links the flat parts.

To evaluate complex expressions we need an algebra that interprets the
logical connectives, i.e. that decides on the valuation of
"A conjunction B" if we know the valuation of A and the valuation of
B. (And so on for all connectives foreseen by the logic's syntax.)

The concept of the triangular norm (t-norm) generalizes "conjunction"
and "intersection" as any binary operator that behaves the way we
expect (commutativity, associativity, identity element, etc).
Similarly t-conorm generalizes "disjunction"/"union" and
"residual" generalized implication. Negation is again called negation.

A t-norm (and company) might be many-valued and continuous in [0..1].

A t-norm (and company) might be many-valued but discete. If, for
instance, a logic had valuations 0, 0.5 , 1 (a "middle" "somewhere in
between" value), a t-norm that is appropriate for interepreting this
logic should be closed in {0, 0.5, 1}.

The norms for four such algebras are:

Zadeh, aka Fuzzy:
t-norm (a and b)    min(a,b)
t-conorm (a or b)   max(a,b)
negation            1-a
redidual (a -> b)   max( 1-a , b )

Lukasiewicz:
t-norm (a and b)    max( a+b-1 , 0 )
t-conorm (a or b)   min( a+b , 1 )
negation            1-1
redidual (a -> b)   min( 1-a+b , 1 )

Goedel:
t-norm (a and b)    min(a,b)
t-conorm (a or b)   max(a,b)
negation            if a=0 then 1, else 0
redidual (a -> b)   if a>b then b, else 1

Product:
t-norm (a and b)    ab
t-conorm (a or b)   a + b - ab
negation            if a=0 then 1, else 0
redidual (a -> b)   if a>b then b/a, else 1


Although quantification would normally be expressed using t-norm
(universal) and t-conorm (existential), it is usually defined using
min, max regardless of the t-norm and t-conorm used for conjunction
and disjunction:

The expression forall R.C is the set (concept) of all instances that
have R only with members of C. So the interpretation of the expession
x : forall R.C is the degree to which all y such that R(x,y) are
members of C:

I(x : forall R.C) = forall y in D . min { I( R(x,y)->C(y) ) }

where I( R(x,y)->C(y) ) is calculated as per the algebra used.

Similarly:

I(x : exists R.C) = forall y in D . max { I( R(x,y) and C(y) ) }

Tableaux reduce the problem to a Integer Linear Programming problem
which is then passed to a solver.


Note that implication is a connective just like any other. We can
assign a valuation to (a->b), besides calculating it from the
valuations of a and b. If we know v(a->b) and v(a), we can calculate
v(b). In this sense v(a->b) is the amount of trust we place on the
assertion that a implies b.