Characterising OWL consistency checkers

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, ...

Received on Friday, 7 March 2003 02:49:54 UTC