OWL DL Syntax (In progress)

Contents

• Introduction
• Design Goals
• Impact on AS&S Design
• Other Differences From AS&S
• The Classification of Properties
• Abstract Syntax Rules
• Mapping Rules
• Triples
• Semantics
• Proofs

Introduction

This paper is based very heavily on the OWL Abstract Syntax and Semantics. It reworks the details of both the abstract syntax and the mapping rules in order that OWL Lite and OWL DL should both be straight forward to specify in terms of which triples are permitted in such graphs. Moreover, the approach taken involves machine processing of the grammar rules so that the correspondence between the two different formulations of the syntax can be verified with mechanical assistance, and maintained.

The design goals are clearly articulated so that design tradeoffs can be discussed and made appropriately.

As well as showing how the OWL DL Design might be improved; this paper also explores the issues to do with annotations and use of rdf:XMLLiteral and xml:lang by taking a significantly different position from AS&S on these points. The discussion is intended to show which parts of the design have been impacted by those different choices. The design goals can be met in the same way, while preserving the choices of Patel-Schneider in AS&S.

Design Goals

Requirements

Clear semantics

Achieved by restricting changes to the abstract syntax to a minimum. This allows the current semantics to be carried forward with very little fuss.

Clear expression of the graphs in the exchange syntax

This is achieved by means of a description not unlike that given in my earlier attempt.

Confidence in the correspondence between the abstract and the concrete syntaxes

Achieved by appropriate automation and proofs.

Desiderata

These are dropped if they conflict with requirements.

High compatibility with RDF(S)

This is reflected in the position taken on annotations, xml:lang and rdf:XMLLiteral.

Syntactic expression of syntactic restrictions

This is stylistic. It is reflected in the desire to not expect the reader to fill in details, so Patel-Schneider's iID becomes my individualID(uriref). Perhaps more significantly this fixes the semantics wrinkle concerning the empty transitive property as a subproperty of every functional property. The cost is that there are more mapping rules in this version than AS&S.

Maintainability

The relationship between the abstract syntax, the mapping rules and RDF graphs is fragile. Having sufficient automated support allows change while ensuring the pieces still all fit together.

Non-Objectives

The items listed here, while desirable, are only permitted in as much as they do not conflict with either the requirements or the desiderata.

Elegance of Abstract Syntax

Changes have been made which are ugly.

Conciseness

The mapping rules are considerable longer. And appear to have much boring repetition. It may be worth revisiting this at some point, since one or two additional variables in the rules might make a big difference to the length.

Liberality of RDF use

In many places the concrete syntax here is significantly stricter than that in AS&S. (For example in requiring all non built-in nodes to have an explicit type). The belief is that it is better to have an intelligible set of rules. Given that AS&S needs more than 80% of nodes to have a type, it is better to make that 100%.

Impact on AS&S Design

Overall, I think there is little change. The abstract syntax is nearly identical, the changes are all fairly subtle; all but one for the worse from the point of view of an abstract syntax. The one that is not for the worse is to do with resolving the transitive property bug. It is fairly ugly, but less ugly than an error.

The main planks of the architecture are still in place: the abstract syntax, the direct semantics, the mapping rules.

The direct expression of OWL Lite and OWL DL graphs is very different; and moreover should be viewed as on the same status as the definition as being the range of the mapping rules. Potential conflict should be addressed by saying that in the event of conflict applications should write to the intersection of the two definitions, and read documents in the range of the mapping rules.

There is one significant change in the semantics, in order to resolve the problem about the meaning of annotations. The change makes annotations have their RDFS meaning, by a direct kludge.

Detailed Differences From AS&S

Abstract Syntax Level

1. In the abstract syntax properties are divided into five types, rather than the two or three (if you count annotations) in AS&S. In the concrete syntax properties are divided into two types rather than the two or three in AS&S.
2. Rules for EquivalentClasses, DisjointClasses, EquivalentIndividuals (and, by mistake, DifferentIndividuals - it is still needed for owl:AllDifferent) have vanished. Being replaced by the somewhat more awkward but essential equivalent productions: classComparison (which may appear on any class or description) and individualComparison (which may appear on named or unnamed individuals). These changes ensure that the bnodes in the resulting graphs can form any sort of tree, but no loops; a characterization that is easy to explain.
3. The ontology can have multiple headers, this is needed to allow owl:imports to work. The version in AS&S is broken, since the triple:
   xxx rdf:type owl:Ontology .
   for the imported ontology is not in the range of the mapping rules.
4. Metaproperties that link ontologies with ontologies are separated from annotations that take other things as their objects. The only permitted metaproperties are the builtin ones defined by OWL (e.g. owl:priorVersion) and also rdfs:isDefinedBy and rdfs:seeAlso (which, alternatively, but not in the same document may be used as annotations)
5. Simple properties, that do not participate in any built-ins except rdfs:subPropertyOf, owl:samePropertyAs, and RDFS annotations, may be used as both annotation properties and as meaningful properties on individuals in the domain of discourse.
6. Unattached descriptions are allowed free-floating as a meaningless directive at the top level - well not quite meaningless since the URIrefs involved in the description are assigned to whatever use they get there. These are needed in the proof of equivalence.
7. Unnamed individuals may be the objects of annotations. Such individuals are treated like facts (i.e. while the annotation itself has no meaning in the direct semantics, the second argument to the annotation does have meaning).
8. literals are taken from RDF Concepts, and are hence more complicated than in AS&S.
9. rdf:XMLLiteral, rdfs:comment, rdfs:label, rdfs:seeAlso, rdfs:isDefined by are all explicitly allowed.
10. Each restriction has to say only one constraint - this makes no difference to the expressive power.
11. Some minor aesthetic changes in the exact choice of rules in the abstract syntax.
12. Added the possibility of declaring dataranges with datarangeIDs. This allows for the use of the same datarange in two places (not permitted in AS&S, which requires verbatim copy). This may require an O(nlogn) computation to verify that two different declarations of the same datarange are the same. (assuming a sort order over the datavalues).
13. Added the possibility of declaring a URI as a datatypeID, as a standalone top-level directive. To make the conditions for and proof of equivalence easier.
14. Added the possibility of declaring a URI as a datarangeID, as a possibly annotated, standalone top-level directive. To make the conditions for and the proof of equivalence easier.

Concrete Syntax Differences

The most visible changes are:

1. new class owl:DataRange, for use in the Ugly test type constructions. The current ugly test bnode does not have a class, since there is no appropriate one.
2. annotations may be used also on individuals. e.g. you can put dc:creator both on the ontology and on a bottle of wine described by the ontology
3. The surface form for owl:priorVersion and friends changes to:

   <owl:Ontology rdf:about="">
      <owl:priorVersion>
         <owl:Ontology rdf:about="old" />
      </owl:priorVersion>
   <owl:Ontology>
   

   This follows the every node must have a class rule. This is also needed on an imports if the imported ontology does not include an ontology header.
4. Really, really, every node has a class (except the builtin urirefs). Those builtins that are like user defined things can be redeclared (e.g. you can redeclare owl:Nothing as an rdfs:Class but not owl:ObjectProperty).
5. I did not include the ability to declare descriptions as of type rdfs:Class. Peter recently added that to AS&S.
6. You can declare something as an owl:TransitiveProperty or owl:SymmetricProperty or owl:InverseFunctionalProperty and that's OK. (The declaration as being an owl:ObjectProperty required by AS&S is dropped, at the cost of a footnote - that's not yet written).

The Classification of Properties

In this abstract syntax properties are classified as of five types:

simple datavalued properties

This may have super and sub properties (the super properties too must be simple datatvalued) the subproperties must be datavalued. They may have equivalent properties. They may not have domain or range constraints, or participate in any restriction, or be declared as functional. They may be used both as annotations and within the ontology on individuals.

simple object properties

This may have super and sub properties (the super properties too must be simple object valued) the subproperties must be object valued. They may have equivalent properties. They may not have domain or range constraints, or participate in any restriction, or be declared as functional, inversefunctional etc. They may be used both as annotations and within the ontology on individuals.

complex datavalued properties

equivalent to the datavalued properties in AS&S.

complex object properties

equivalent to the non-transitive individual valued properties in AS&S.

transitive properties

equivalent to the individual valued properties in AS&S that do not participate in cardinality constraints.

Having these five categories allows the following advantages over AS&S:

1. The side condition that is incorrectly expressed in AS&S can be expressed appropriately (i.e. syntactically).
2. What annotations are allowed is clarified.
3. Facility is provided for user definition of annotations
4. It is permitted to use general properties like rdfs:comment, dc:creator and rdfs:label on individuals, classes properties and ontologies.

The following disadvantages are apparent:

1. There is an apparent complexification of the abstract syntax (but not at the concrete level).
2. There are significantly more mapping rules, partly as a result.

Abstract Syntax Rules

There is still a lot of mechanical checking to do on this grammar.

The following table was generated by a program working from a machine readable version of the mapping rules. (all done in Prolog).

ontology    [O1] ::= 'Ontology(' { directive } ')'

Rationale: When dealing with imports, the resulting ontology may many header blocks, with many different ontologyID URI references. Hence, the change from the published AS&S.

directive   [V1] ::= header
            [V2] | axiom
            [V3] | fact

header      [H1] ::= 'Header(' ontologyID { metaProperty } { annotation } ')'

The only metaproperties are: owl:imports, owl:backwardsCompatibleWith, etc. There is no facility for user-defined metaproperties.

metaProperty[M1] ::= 'MetaProperty(' metapropertyID ontologyID ')'

annotation  [A1] ::= 'Annotation(' simpleDataPropID dataLiteral ')'

Wherever in an abstract syntax document the following rule is used, the individual is also treated as a top-level fact .

annotation  [A2] ::= 'Annotation(' simpleObjectPropID individual ')'

fact        [F1] ::= individual

individual  [I1] ::= 'Individual(' [ individualID ] { 'Type(' type ')' } 
                         { propertyValue } { individualComparison } ')'

propertyValue[P1] ::= 'PropertyValue(' simpleObjectPropID individual ')'
            [P2] | 'PropertyValue(' complexObjectPropID individual ')'
            [P3] | 'PropertyValue(' transitivePropID individual ')'
            [P4] | 'PropertyValue(' simpleDataPropID dataLiteral ')'
            [P5] | 'PropertyValue(' complexDataPropID dataLiteral ')'

type        [T1] ::= classID
            [T2] | restriction

This maps directly onto RDF literals and has the same constraints and definitions. See [RDF Concepts]. Note, specifically that there the lexicalForm is in Unicode Normal Form C, and that the language identifier is an RFC 3066 language tag normalized to lower case.

The formatting of the symbols lexicalForm and language is in error.

dataLiteral [L1] ::= 'DataLiteral(' lexicalForm [ language ] [ datatypeID ] ')'

individualComparison[I1] ::= 'SameIndividual(' individual ')'
            [I2] | 'DifferentIndividuals(' individual ')'

{comparison} is in this rule, primarily for use in OWL DL. In the OWL Lite context, it is clearer to have an EquivalentClasses axiom (as in the published abstract syntax.

axiom       [X1] ::= 'Class(' classID modality { annotation } 
                         { 'Super(' type ')' } { classComparison } ')'

modality    [M1] ::= partial

classComparison[C1] ::= 'SameClassAs(' classID ')'

Rationale: This differs from the published AS&S in that each restriction may only contain one condition, not an arbitrary number. The expressive power is unchanged, since every use may be repeated arbitrarily. This makes it easier to express the mapping to RDF in which each condition becomes a separate blank node.

restriction [R1] ::= 'Restriction(' complexDataPropID 'AllValuesFrom(' dataRange ')' ')'
            [R2] | 'Restriction(' complexDataPropID 'SomeValuesFrom(' dataRange ')' ')'
            [R3] | 'Restriction(' complexDataPropID 'Cardinality(' smallInt ')' ')'
            [R4] | 'Restriction(' complexDataPropID 'MinCardinality(' smallInt ')' ')'
            [R5] | 'Restriction(' complexDataPropID 'MaxCardinality(' smallInt ')' ')'
            [R6] | 'Restriction(' complexObjectPropID 'AllValuesFrom(' classInRestriction ')' ')'
            [R7] | 'Restriction(' complexObjectPropID 'SomeValuesFrom(' classInRestriction ')' ')'
            [R8] | 'Restriction(' complexObjectPropID 'Cardinality(' smallInt ')' ')'
            [R9] | 'Restriction(' complexObjectPropID 'MinCardinality(' smallInt ')' ')'
            [R10] | 'Restriction(' complexObjectPropID 'MaxCardinality(' smallInt ')' ')'
            [R11] | 'Restriction(' transitivePropID 'AllValuesFrom(' classInRestriction ')' ')'
            [R12] | 'Restriction(' transitivePropID 'SomeValuesFrom(' classInRestriction ')' ')'

axiom       [X2] ::= restriction

Rationale: The extra level here is used for an extension in OWL DL.

classInRestriction[S1] ::= classID

smallInt    [S1] ::= 0
            [S2] | 1

dataRange   [G1] ::= datatypeID
            [G2] | dataRangeID

axiom       [X3] ::= 'DatatypeProperty(' simpleDataPropID { annotation } 
                         { 'Super(' simpleDataPropID ')' } ')'

Rationale: For ease of writing the document, I have made the property axioms identical in OWL Lite and OWL DL, but kept the same semantics by having the additional rules for dataRange and classInRestriction in OWL DL

axiom       [X4] ::= 'DatatypeProperty(' complexDataPropID { annotation } 
                         { 'Super(' simpleDataPropID ')' } { 'Super(' complexDataPropID ')' } 
                         { 'Domain(' classInRestriction ')' } 
                         { 'Range(' dataRange ')' } [ functional ] ')'
            [X5] | 'IndividualProperty(' simpleObjectPropID 
                         { annotation } { 'Super(' simpleObjectPropID ')' } ')'
            [X6] | 'IndividualProperty(' complexObjectPropID 
                         { annotation } { 'Super(' simpleObjectPropID ')' } 
                         { 'Super(' complexObjectPropID ')' } 
                         { 'Super(' transitivePropID ')' } { 'Domain(' classInRestriction ')' } 
                         { 'Range(' classInRestriction ')' } 
                         { 'Inverse(' complexObjectPropID ')' } 
                         [ functional ] [ inverseFunctional ] 
                         [ symmetric ] ')'
            [X7] | 'IndividualProperty(' transitivePropID { annotation } 
                         { 'Super(' simpleObjectPropID ')' } 
                         { 'Super(' transitivePropID ')' } { 'Domain(' classInRestriction ')' } 
                         { 'Range(' classInRestriction ')' } 
                         { 'Inverse(' transitivePropID ')' } 
                         [ transitive ] ')'
            [X8] | 'EquivalentProperties(' simpleObjectPropID 
                         simpleObjectPropID { simpleObjectPropID } ')'
            [X9] | 'EquivalentProperties(' transitivePropID 
                         transitivePropID { transitivePropID } ')'
            [X10] | 'EquivalentProperties(' complexObjectPropID 
                         complexObjectPropID { complexObjectPropID } ')'
            [X11] | 'EquivalentProperties(' simpleDataPropID 
                         simpleDataPropID { simpleDataPropID } ')'
            [X12] | 'EquivalentProperties(' complexDataPropID 
                         complexDataPropID { complexDataPropID } ')'
            [X13] | 'DatatypeDeclaration(' datatypeID ')'

OWL DL Incremental Abstract Syntax

type        [T3] ::= description

modality    [M2] ::= complete

axiom       [X14] ::= 'EnumeratedClass(' classID { annotation } 
                         { individualID } ')'

classComparison[C2] ::= 'SameClassAs(' description ')'
            [C3] | 'DisjointWith(' description ')'
            [C4] | 'SubClassOf(' description ')'

description [D1] ::= classID
            [D2] | restriction
            [D3] | 'UnionOf(' { description } { classComparison } ')'
            [D4] | 'IntersectionOf(' { description } { classComparison } ')'
            [D5] | 'ComplementOf(' description { classComparison } ')'
            [D6] | 'OneOf(' { individualID } { classComparison } ')'

axiom       [X15] ::= description

restriction [R13] ::= 'Restriction(' complexDataPropID 'Value(' dataLiteral ')' ')'
            [R14] | 'Restriction(' complexObjectPropID 'Value(' individualID ')' ')'
            [R15] | 'Restriction(' transitivePropID 'Value(' individualID ')' ')'

smallInt    [S3] ::= naturalNumber

These rules broadens the scope of restrictions, domain and range conditions.

classInRestriction[S2] ::= description

dataRange   [G3] ::= 'OneOf(' { dataLiteral } ')'

Rationale: Using the same dataRange in multiple range constraints of restrictions requires too much repetition without allowing dataRangeID .

axiom       [X16] ::= 'DataRange(' dataRangeID { annotation } { dataLiteral } ')'

Rationale: A datarange declaraion which does not identify the individuals is not useful, except perhaps to document the intended range of a datatype property. However, it does make the proofs easier, and the special cases fewer.

axiom       [X17] ::= 'DataRange(' dataRangeID declaration { annotation } ')'

OWL DL Complete Abstract Syntax

ontology    [O1] ::= 'Ontology(' { directive } ')'

directive   [V1] ::= header
            [V2] | axiom
            [V3] | fact

header      [H1] ::= 'Header(' ontologyID { metaProperty } { annotation } ')'

metaProperty[M1] ::= 'MetaProperty(' metapropertyID ontologyID ')'

annotation  [A1] ::= 'Annotation(' simpleDataPropID dataLiteral ')'
            [A2] | 'Annotation(' simpleObjectPropID individual ')'

fact        [F1] ::= individual

individual  [I1] ::= 'Individual(' [ individualID ] { 'Type(' type ')' } 
                         { propertyValue } { individualComparison } ')'

propertyValue[P1] ::= 'PropertyValue(' simpleObjectPropID individual ')'
            [P2] | 'PropertyValue(' complexObjectPropID individual ')'
            [P3] | 'PropertyValue(' transitivePropID individual ')'
            [P4] | 'PropertyValue(' simpleDataPropID dataLiteral ')'
            [P5] | 'PropertyValue(' complexDataPropID dataLiteral ')'

type        [T1] ::= classID
            [T2] | restriction
            [T3] | description

dataLiteral [L1] ::= 'DataLiteral(' lexicalForm [ language ] [ datatypeID ] ')'

individualComparison[I1] ::= 'SameIndividual(' individual ')'
            [I2] | 'DifferentIndividuals(' individual ')'

axiom       [X1] ::= 'Class(' classID modality { annotation } 
                         { 'Super(' type ')' } { classComparison } ')'
            [X2] | restriction
            [X3] | 'DatatypeProperty(' simpleDataPropID { annotation } 
                         { 'Super(' simpleDataPropID ')' } ')'
            [X4] | 'DatatypeProperty(' complexDataPropID { annotation } 
                         { 'Super(' simpleDataPropID ')' } { 'Super(' complexDataPropID ')' } 
                         { 'Domain(' classInRestriction ')' } 
                         { 'Range(' dataRange ')' } [ functional ] ')'
            [X5] | 'IndividualProperty(' simpleObjectPropID 
                         { annotation } { 'Super(' simpleObjectPropID ')' } ')'
            [X6] | 'IndividualProperty(' complexObjectPropID 
                         { annotation } { 'Super(' simpleObjectPropID ')' } 
                         { 'Super(' complexObjectPropID ')' } 
                         { 'Super(' transitivePropID ')' } { 'Domain(' classInRestriction ')' } 
                         { 'Range(' classInRestriction ')' } 
                         { 'Inverse(' complexObjectPropID ')' } 
                         [ functional ] [ inverseFunctional ] 
                         [ symmetric ] ')'
            [X7] | 'IndividualProperty(' transitivePropID { annotation } 
                         { 'Super(' simpleObjectPropID ')' } 
                         { 'Super(' transitivePropID ')' } { 'Domain(' classInRestriction ')' } 
                         { 'Range(' classInRestriction ')' } 
                         { 'Inverse(' transitivePropID ')' } 
                         [ transitive ] ')'
            [X8] | 'EquivalentProperties(' simpleObjectPropID 
                         simpleObjectPropID { simpleObjectPropID } ')'
            [X9] | 'EquivalentProperties(' transitivePropID 
                         transitivePropID { transitivePropID } ')'
            [X10] | 'EquivalentProperties(' complexObjectPropID 
                         complexObjectPropID { complexObjectPropID } ')'
            [X11] | 'EquivalentProperties(' simpleDataPropID 
                         simpleDataPropID { simpleDataPropID } ')'
            [X12] | 'EquivalentProperties(' complexDataPropID 
                         complexDataPropID { complexDataPropID } ')'
            [X13] | 'DatatypeDeclaration(' datatypeID ')'
            [X14] | 'EnumeratedClass(' classID { annotation } 
                         { individualID } ')'
            [X15] | description
            [X16] | 'DataRange(' dataRangeID { annotation } { dataLiteral } ')'
            [X17] | 'DataRange(' dataRangeID declaration { annotation } ')'

modality    [M1] ::= partial
            [M2] | complete

classComparison[C1] ::= 'SameClassAs(' classID ')'
            [C2] | 'SameClassAs(' description ')'
            [C3] | 'DisjointWith(' description ')'
            [C4] | 'SubClassOf(' description ')'

restriction [R1] ::= 'Restriction(' complexDataPropID 'AllValuesFrom(' dataRange ')' ')'
            [R2] | 'Restriction(' complexDataPropID 'SomeValuesFrom(' dataRange ')' ')'
            [R3] | 'Restriction(' complexDataPropID 'Cardinality(' smallInt ')' ')'
            [R4] | 'Restriction(' complexDataPropID 'MinCardinality(' smallInt ')' ')'
            [R5] | 'Restriction(' complexDataPropID 'MaxCardinality(' smallInt ')' ')'
            [R6] | 'Restriction(' complexObjectPropID 'AllValuesFrom(' classInRestriction ')' ')'
            [R7] | 'Restriction(' complexObjectPropID 'SomeValuesFrom(' classInRestriction ')' ')'
            [R8] | 'Restriction(' complexObjectPropID 'Cardinality(' smallInt ')' ')'
            [R9] | 'Restriction(' complexObjectPropID 'MinCardinality(' smallInt ')' ')'
            [R10] | 'Restriction(' complexObjectPropID 'MaxCardinality(' smallInt ')' ')'
            [R11] | 'Restriction(' transitivePropID 'AllValuesFrom(' classInRestriction ')' ')'
            [R12] | 'Restriction(' transitivePropID 'SomeValuesFrom(' classInRestriction ')' ')'
            [R13] | 'Restriction(' complexDataPropID 'Value(' dataLiteral ')' ')'
            [R14] | 'Restriction(' complexObjectPropID 'Value(' individualID ')' ')'
            [R15] | 'Restriction(' transitivePropID 'Value(' individualID ')' ')'

classInRestriction[S1] ::= classID
            [S2] | description

smallInt    [S1] ::= 0
            [S2] | 1
            [S3] | naturalNumber

dataRange   [G1] ::= datatypeID
            [G2] | dataRangeID
            [G3] | 'OneOf(' { dataLiteral } ')'

description [D1] ::= classID
            [D2] | restriction
            [D3] | 'UnionOf(' { description } { classComparison } ')'
            [D4] | 'IntersectionOf(' { description } { classComparison } ')'
            [D5] | 'ComplementOf(' description { classComparison } ')'
            [D6] | 'OneOf(' { individualID } { classComparison } ')'

Mapping Rules

Still to do:

• footnotes
• lists
• verifying (mechanically) that all the rules make sense

The following table was generated by a program working from a machine readable version of the mapping rules. (all done in Prolog).

Triples

This section is still to be started.

The basic format will be like in the message I sent with an early draft.

The conditions on the types have been simplified. The new tables will be generated automatically from the mapping rules.

Semantics

To fix the problem of annotations and entailments, the definition of entailment between RDF/XML files is changed to approximately:

Given an RDF file X with abstract syntax representation X' and an RDF file Y with abstract syntax representation Y', then X X DL-entails Y if and only if both X' direct-entails Y' and X rdfs-entails the subset of Y consisting of the annotation triples.

RDFS compatible semantics are clarified to say that:

• owl:TransitiveProperty, owl:SymmetricProperty, owl:InverseFunctionalProperty are all sub classes of owl:ObjectProperty (Also for the DL semantics)
• In OWL full it is clarified that owl:ObjectProperty is the same class as rdf:Property.

Proofs

Just at the beginning stages - all things needing mechanical verification have not been verified.

This version doesn't distinguish between DL and Lite.

Terminology

An A-graph is an RDF graph that is the result of mapping an abstract syntax ontology using the mapping rules. (An A-graph is finite).

A T-graph is a finite RDF graph that obeys the rules (no blank loops, no bnode as the object of two or more triples, every node either builtin or with an explicit type, excluding rdfs:Class, rdf:Property, owl:FunctionalProperty, owl:DeprecatedClass, owl:DeprecatedProperty), and for which there exists some classification of nodes into categories that arise in the abstract syntax, such that every triple is in the long list of triples (not yet ) in the previous section. All bnodes of type rdf:List must be the object of some triple. Moreover in a T-graph the blank nodes are tightly constrained, as described in the previous section.

Lemma 1: necessity

Every A-graph is a T-graph.

the proof is wholly straightforward and mechanical and reflects the way the triple table is generated. It is probably quite tedious.

Lemma 2: ground type only graphs

Every ground T-graph all of whose triples have predicate rdf:type is an A-graph.

Proof, from a mechanical generated list table given for any such type triple, a directive from the abstract syntax that corresponds to just that one triple.

Lemma 3: bnode locations

If a ground T-graph contains a bnode then it contains either a bnode that is not the object of any triple, or a bnode which is the object of a triple with a uriref subject.

Lemma 4: empty graph

The empty graph is both a T-graph and an A-graph

Lemma 5: ground triples

Given any ground non-type triple in a T-graph you can construct an abstract syntax directive that corresponds to exactly that triple and some type triples that are necessarily in the T-graph

Proof again is a mechanically generated list

Theorem a graph is a T-graph iff it is an A-graph

Lemma 1 is half the problem done.

We proceed by induction from lemma 4

Suppose t is a T-graph and for all smaller T-graph are A-graphs (and that the node classifications match - need to expand this bit), then, one of the following holds:

1. Every triple is a type triple, and we are done.
2. There is a ground non-type triple, and we are done. We remove it, the graph is smaller. We take the abstract syntax for the smaller graph, and the abstract syntax for the single triple (by lemma 5) and merge them.
3. There is a bnode, which without loss of generality (by lemma 3) is either the object of a triple with a uriref subject or the object of no triples. There are not so many different cases to consider, and we work through them all rather laboriously (with mechanical assistence).