Syntax proof

I have done a first version of a sufficiency proof.

I am sorry it has taken so long, it was significantly harder than I had 
imagined (or perhaps I've just made a pig's ear of it).


It is still missing some machine generated tables, which I hope to add 
later today. I also need to do my own review of the proof, which I hope 
will permit me to shorten it - I also believe that there are bugs 
concerning literal objects.

(The bulk of the code for the tables is written, it is naive and slow - it 
takes hours to run).

The necessity proof would be easier, and I am less worried about it, since 
the triple tables are generated from the mapping rules.

The URL for the proofs are changed:

http://www.w3.org/2001/sw/WebOnt/syntaxTF/prolog/out/dl/proof1.html
http://www.w3.org/2001/sw/WebOnt/syntaxTF/prolog/out/lite/proof1.html

====
More detailed comment:


When I was seventeen my school maths report was
A, A, "Jeremy is overly fond of algebraic drapery."

I fear that my maths teacher is still correct!

Working on the proof resulted in a few substantive changes listed
below, and greater insight into a philosophical difference between
my text and Peter's which I explore in the next message (after lunch).


Substantive Changes made:
1: treatment of type on individualIDs and unnamedIndividuals changed
   Motives: (a) bug fix
            (b) making proof easier
   Now much closer to Peter
   (requiring a type is a constraint on mapping as a whole,
    two rules optional produce rdf:type owl:Thing
    I believe Peter did have exactly this scheme at one point,
    he currently is expressing optionality by not accepting the
    map of an abstract syntax tree that does not assign a type
    to an individual).

2: unnamedDataRange declaration
   similarly to the meaningless directives for
   toplevel descriptions and restrictions, I added a
   toplevel directive (DL only) for unnamed dataranges.
   This arose while working on the proof, rationale in next
   message. While this increases the differences between
   Peter's text and mine, it does not increase the number
   of points to discuss because this is one and the same
   philosophical difference, and we should probably either
   accept or reject all three of these meaningless top-level
   directives that I propose.

3: (minor) I changed the expression of an unnamed datarnage in the
   abstract syntax from oneOf({dataLiteral}) to dataRange({dataLiteral})
   This avoids ambiguity when mapping oneOf() as to whether that is
   the empty enumeration of dataLiterals or the empty enumeration
   of individuals. (Semantically the same, but of different syntactic
   category).

4: datatype declaration
   In my earlier draft I had a directive in the abstract syntax that
   Peter does not have viz:
   axiom ::= ...
   [M11] | DatatypeDeclaration(  datatypeID  )

   I had forgot to map it (it goes to
     datatypeID rdf:type rdfs:Datatype .
     optional for xsd builtins.
     non xsd builtins only allowed in OWL DL?
   )
   I have switched this to be a directive (it really isn't an
   axiom).

   Peter's text has suffered from a defect (IMO) that
   you must have type triples for datatypes if and only
   if that datatype is used somewhere other than in
   a cardinality constraint.
   This directive is intended to allow unused datatype
   declarations.

   The simplest resolution of this problem, which I suspect
   neither I nor Peter want, is that we note that the only
   datatypes we support are xsd:builtins and they do not
   need such declarations, and so we can simply omit
   these from OWL DL and OWL Lite, (and rdfs:Datatype
   would not appear in OWL Lite or OWL DL graphs).

   As is, this construct needs a note to the effect that
   it is intended for use with user defined datatypes
   (but permitted for redundant declarations of
   xsd datatypes).
   The user defined types are
   either provided by an XSD or RDF future mechanism,
   or by private agreement. (I would not oppose
   further describing the private agreement used in
   DAML+OIL).

e.g.

   NOTE: OWL does not support the mechanism for
   user defined datatypes found in DAML+OIL, which
   is ... (text from an earlier e-mail msg of Peter's).

or more positively

   NOTE: DAML+OIL provided a mechanism for
   user defined datatypes which can be viewed
   as such a private agreement. It is likely to
   be superceded by a mechanism suggested by the
   W3C. The DAML+OIL mechanism is ... (text from an earlier
   e-mail msg of Peter's).

(HP interest: Jena currently supports the DAML+OIL mechanism
and we do not intend to deprecate it until there is a replacement).

Jeremy

Received on Monday, 3 March 2003 12:39:22 UTC