# Test whether a schema mentions the predicates used in this data # This involves searching in files for statements being present or absent. @prefix rdf: . @prefix s: . # @prefix dpo: . @prefix log: . @prefix os: . @prefix : . # Local stuff @prefix val: . # Local stuff # Usage: TARGET=myfile.n3 cwm check.n3 -think -purge # # Output should not incldue any error messages. # @forAll :d, :o, :p, :r, :s, :S, :s1, :x, :y, :F, :G, :H. # Some internal terms we will be using in this document: :usedAsPropertyIn a rdf:Property; s:comment "This term is used as a Property in the given document."; a log:Chaff. # Internal use only, may be purged. :within a rdf:Property; s:comment "relationship between a subforumula and the document it was found in"; a log:Chaff. # Internal use only, may be purged. :targetDocument a s:Class; s:comment "Documents which this run is checking for schema validity"; a log:Chaff. # Internal use only, may be purged. :propertySchema a rdf:Property; s:comment "The schema for a Property is the document which defines it.". :ERROR_NO_SCHEMA_OR_NOT_DECLARED a rdf:Property; s:comment """The document used this as a predicate and there is no schema which declares it as a Property""". :ERROR_PROPERTY_NOT_DECLARED a rdf:Property. # Target formulae are the top level formula we are pointed at, # and any subformulae. { :d log:uri [is os:environ of "TARGET"] } log:implies { :d a :targetDocument }. { :d a :targetDocument. :d log:semantics :F } log:implies { :F :within :d }. # Define subforumulae which are within the target documents: { :d a :targetDocument. :F :within :d. :F log:includes { :s :p :o}. :s log:rawType log:Formula } log:implies { :s :within :d } . { :d a :targetDocument. :F :within :d. :F log:includes { :s :p :o}. :o log:rawType log:Formula } log:implies { :o :within :d } . # Anything used as a predicate in any target formula should be checked. # We don't bother bout the pseudoproperties log:forSome and log:forAll. { :d a :targetDocument. :F :within :d. :F log:includes { :s :p :o}. :p log:rawType log:Other. # Ignore lists :p log:notEqualTo log:forSome, log:forAll } log:implies { :p :usedAsPropertyIn :d } . # Let's see what happens when we dereference a predicate: { :d a :targetDocument. :p :usedAsPropertyIn :d. :p log:semanticsOrError :x } log:implies { :p :predicateSemanticsOrError :x }. { :d a :targetDocument. :p :usedAsPropertyIn :d. :p :predicateSemanticsOrError :x. :x log:rawType log:Literal } log:implies { :d :ERROR_IN_SCHEMA_ACCESS_FOR :p. :p :SCHEMA_ACCESS_ERROR :x }. { :p :predicateSemanticsOrError :x. :x log:rawType log:Formula } log:implies { :p :semanticsOK :x }. # The RDFS spec implies the following algorithm for the definitive schema corresponding # to a Property :p. (From Ralph Swick, whiteboard conversation) # Maybe we should simplify it to the schema being the result of dereferencing the Property? # I think the counterexample is the dublin core, but it may not work anyway. # Actually, the dublic core uses a redirect!!! We need to be aware of the # existence of redirects like that @@ { :d a :targetDocument. :p :usedAsPropertyIn :d. :p :semanticsOK [log:includes { :p s:isDefinedBy :s }]. } log:implies { :p :propertySchema :s. :d :documentSchema :s. }. # The normal case is with no redirection: { :d a :targetDocument. :p :usedAsPropertyIn :d. :p :semanticsOK [log:notIncludes { :p s:isDefinedBy [] }]. :p log:racine :s. } log:implies { :p :propertySchema :s. :d :documentSchema :s. }. # We actually need the formula the schema parses to: { :p :propertySchema [ :semanticsOK :F ] } log:implies { :p :schemaFormula :F }. { :d :documentSchema :s. :s :semanticsOK :F. (:F [is log:semantics of ]) log:conjunction [has log:conclusion :G]. } log:implies { :s :augmented :G } # We don't insist that the schema *directly* defined properties and # classes as such. We take as given the axioms of rdfs. # Here, we consider an augmented schema which is the deductive closure # of the original schema and the axioms: { ( [is :schemaFormula of :p] [is log:semantics of ] ) log:conjunction [ has log:conclusion :G ] } log:implies { :p :augmentedSchemaFormula :G }. # It is an error, we say, for something to be used as a Property but # not im plicitly or explicitly declared as such in the schema, that is, # not explicitly declared as such in the augmented schema. # # (That is, except for local identifiers, which we assume to be used correctly. # Note this looseness is a choice: we could require local declarations, # to follow a more traditionally careful software engineering style.) { :d a :targetDocument. :p :usedAsPropertyIn :d; log:racine [log:notEqualTo :d]. # Not local :p :schema [:augmented [log:notIncludes { :p a rdf:Property }]]. } log:implies { :d :ERROR_PREDICATE_NOT_DECLARED_AS_PROPERTY :p }. # (b)when the document is combined with the above, no contradiction # can be found from anything being (eg) member of disjoint sets. # { :d a :targetDocument. :p :usedAsPropertyIn :d; :augmentedSchemaFormula :F} log:implies { :d :usesAugmented :F }. { :d :usesAugmented :F. ( [is log:semantics of :d] :F ) log:conclusion [log:includes ([] a :ERROR)] } log:implies { :d :ERROR_INCONSISTENCY_W_R_T_SCHEMA :s } @@@ ################################################################### Clean up {:d a :targetDocument. :F :within :d } log:implies { :F a log:Chaff }. # Clear our formulae log:Chaff is rdf:type of rdf:type, # Seriously ... s:comment, log:forAll, log:implies, # Clear out rules on -purge :within, :schemaFormula, :augmentedSchemaFormula, :propertySchema, :predicateSemanticsOrError, :semanticsOK, # :targetDocument, :usedAsPropertyIn. #ends