@prefix dc: .
<> dc:title "Infoset Utilites";
dc:source ;
dc:description """rules and such...""".
@prefix iu: .
@prefix dl: .
@prefix sws: .
@prefix dpo: .
@prefix rdf: .
@prefix rdfs: .
@prefix log: .
@prefix is: . #@@ move this there.
@prefix : <#>. #variables
iu:AbsoluteURIref rdfs:label "Abs. URIref";
rdfs:subClassOf rdfs:Literal;
rdfs:comment "@@hmm... before or after %xx-ing unicode chars?";
rdfs:comment "@@connect with XML Schema data type and/or 03swell/URI stuff.".
iu:AbsoluteURI rdfs:label "Absolute URI";
rdfs:subClassOf iu:AbsoluteURIref;
rdfs:comment "@@hmm... before or after %xx-ing unicode chars?".
iu:String rdfs:label "String";
rdfs:subClassOf rdfs:Literal;
rdfs:comment "@@connect with XML Schema data type stuff".
iu:Boolean rdfs:label "Boolean";
rdfs:subClassOf rdfs:Literal;
dpo:oneOf ( iu:true iu:false );
rdfs:comment "@@connect with XML Schema data type stuff".
iu:true rdfs:label "true".
iu:false rdfs:label "false".
rdfs:Literal rdfs:label "Literal".
iu:EncName rdfs:label "EncName";
iu:pattern "[A-Za-z][A-Za-z0-9._-]*"; #@@ double-check this.
rdfs:isDefinedBy ;
rdfs:subClassOf iu:Name;
rdfs:comment"production [81] from the XML spec".
iu:Name rdfs:label "Name";
iu:pattern "@@";
rdfs:subClassOf iu:String;
rdfs:comment"production [@@] from the XML spec".
iu:NCName rdfs:label "NCName";
iu:pattern "@@";
rdfs:subClassOf iu:Name;
rdfs:comment"production [@@] from the Namespaces in XML spec".
#@@@iu:Prefix rdfs:label "Prefix";
# dpo:disjointUnionOf (iu:NoValue iu:NCName).
iu:VersionNum rdfs:label "VersionNum";
iu:pattern "[a-zA-Z0-9_.:-]+";
rdfs:subClassOf iu:String;
rdfs:isDefinedBy .
iu:pattern rdfs:label "pattern";
rdfs:comment "@@xml schema datatype facet";
rdfs:domain rdfs:Class.
iu:StandAloneType rdfs:label "Standalone Type";
dpo:oneOf ( is:yes is:no ).
iu:NoValue rdfs:label "No Value";
dpo:oneOf ( is:noValue ). #@@ cf bottom in KIF v3
## Logic utilities...
#@@{ :P log:means :Q } log:implies { :P log:implies :Q. :Q log:implies :P. }.
# explain a bit of daml...
dpo:toClass rdfs:range rdfs:Class.
dpo:toClass rdfs:domain rdfs:Class.
this log:forAll :C1, :s, :p, :o, :L, :C2.
{ :C1 dpo:disjointUnionOf :L.
:L dl:member :C2 }
log:implies { :C2 rdfs:subClassOf :C1 }.
{ :s a [ dpo:onProperty :p; dpo:hasValue :o ]. }
log:implies { :s :p :o }.
dpo:oneOf rdfs:domain rdfs:Class.
#@@ { :C1 dpo:oneOf :L.
# :L dl:member :x.
#}
# log:implies { :x a :L }.
# some rdfs rules...
rdfs:domain rdfs:domain rdfs:Class.
rdfs:range rdfs:domain rdfs:Class.
this log:forAll :s, :p, :o, :C.
#subproperty
{ :s [ rdfs:subPropertyOf :p ] :o. }
log:implies { :s :p :o }.
#subclass
{ :s rdf:type [ rdfs:subClassOf :C ] }
log:implies { :s rdf:type :C. }.
rdfs:subClassOf rdfs:domain rdfs:Class.
# (part of?) the definition of rdfs:domain...
{ :s :p :o.
:p rdfs:domain :C. } log:implies { :s a :C }.
# transitivity of subClassOf
{ :s rdfs:subClassOf [ rdfs:subClassOf :o ] }
log:implies { :s rdfs:subClassOf :o }.