Re: Characterising OWL consistency checkers

On March 7, Jim Hendler writes:
> 
> At 0:34 +0000 3/7/03, Ian Horrocks wrote:
> >I accepted the task of trying to find some words to describe the
> >properties of OWL consistency checkers, in particular
> >w.r.t. datatypes.
> >
> >While I was about it, it occurred to me that what was really required
> >was a semantic characterisation of what it means to "support" a given
> >datatype. The way I propose to do this would have the advantage that
> >an OWL consistency checker would "handle" ALL datatypes, and would
> >simply provide more inferential power for supported datatypes; it also
> >makes it very straightforward to describe the properties of OWL
> >consistency checkers.
> >
> >Here it is...
> >
> >
> >Preface
> >=======
> >
> >I want to propose a small extension of the AS&S that:
> >
> >1. Fixes what I consider to be an infelicity in the way data values
> >are treated, by having "invalid" typed data values (e.g.,
> >"257"^^xsd:byte) be treated in a similar way to the combination of an
> >untyped data value and an inferred type (e.g., "257"^^xsd:int and, by
> >the way, it is a byte). Currently, the first is NOT logically
> >inconsistent, while the second is. The proposal would result in both
> >being logically inconsistent.
> >
> >2. Formalises the notion of "unsupported" datatypes. For an
> >unsupported datatype, data values are interpreted as resources that
> >are in the union LV and the complement of R (i.e., they are either
> >values or "junk"). Two syntactically identical data values have the
> >same interpretation; for non-identical data values, nothing is known
> >(they do NOT necessarily have different interpretations).
> >
> >
> >With these extensions, describing the properties of an OWL consistency
> >checker becomes relatively straightforward:
> >
> >OWL Consistency Checkers
> >========================
> >
> >An OWL consistency checker takes a document as input, and outputs one
> >word: Consistent, Inconsistent, or Unknown.
> >
> >An OWL document is Consistent iff there exists some MODEL of the
> >document that is consistent with the constraints specified by the
> >relevant MODEL THEORY (pointer to ASS).
> >
> >An OWL consistency checker MUST return "Consistent" only when the
> >input document is consistent and "Inconsistent" only when the input
> >document is not consistent (this property is usually called
> >SOUNDNESS).
> >
> >An OWL consistency checker is COMPLETE if, given sufficient (but
> >finite) resources (CPU cycles and memory), it will always return
> >either Consistent or Inconsistent; otherwise it is INCOMPLETE. It has
> >been shown that for OWL Lite and DL it is possible to construct a
> >complete consistency checker (the languages are DECIDABLE), and that
> >for OWL full it is not possible to construct a complete consistency
> >checker (the language is UNDECIDABLE).
> >
> >An OWL consistency checker SHOULD support at least the following XMLS
> >datatypes: integer, string, ...
> 
> Ian -
>   I think this is valuable, but doesn't quite solve the problem of 
> specifying how much inferencing is required with respect to 
> datatypes.  I think that is because you say the consistency checker 
> SHOULD "support" -- but what we need is a definition of that support.

The beauty of the proposal is that the model theory interprets ALL
datatypes/values, with supported datatypes/values simply having more
constraints on their interpretation - so the MT formalises what it
means to support a datatype.
 
> For example, if we said an OWL consistency checker is expected to be 
> sound with respect to the xsd:datatypes listed in Guide, that would 
> suffice and be something doable (and we would have implementations 
> that already handle it).  Or we could say SOUND on all of them and 
> complete with respect to strings and integers (essentially the OIL 
> criteria)

Because ALL datatypes/values are interpreted, an OWL reasoner MUST
"deal with" all datatypes. This isn't a big overhead because
unsupported datatypes can be treated in a uniform and very lightweight
manner. If a reasoner claims to support a given datatype, AND it
claims to be complete, then it has to do more work w.r.t. that
datatype (the MT formalises just what it has to do).

>   but we need some decision on this

The decision as to which datatypes (if any) MUST be supported by all
OWL reasoners is obviously one that has to be made by the working
group. My suggestion is that we make this a fairly short (possibly
zero length) list.

Ian



>   -JH
> 
> 
> -- 
> Professor James Hendler				  hendler@cs.umd.edu
> Director, Semantic Web and Agent Technologies	  301-405-2696
> Maryland Information and Network Dynamics Lab.	  301-405-6707 (Fax)
> Univ of Maryland, College Park, MD 20742	  240-731-3822 (Cell)
> http://www.cs.umd.edu/users/hendler
>

Received on Friday, 7 March 2003 13:02:00 UTC