{-# LANGUAGE OverloadedStrings #-} -------------------------------------------------------------------------------- -- See end of this file for licence information. -------------------------------------------------------------------------------- -- | -- Module : ProofContext -- Copyright : (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011, 2012 Douglas Burke -- License : GPL V2 -- -- Maintainer : Douglas Burke -- Stability : experimental -- Portability : OverloadedStrings -- -- This module contains proof-context declarations based on -- the RDF, RDFS, and RDF datatyping semantics specifications. -- These definitions consist of namespaces (for identification -- in proofs), axioms and inference rules. -- -------------------------------------------------------------------------------- module Swish.RDF.ProofContext ( rulesetRDF , rulesetRDFS , rulesetRDFD) where import Swish.Datatype (typeMkCanonicalForm) import Swish.Namespace (Namespace, makeNSScopedName) import Swish.QName (LName) import Swish.Ruleset (makeRuleset) import Swish.VarBinding (VarBindingModify(..)) import Swish.VarBinding (applyVarBinding, addVarBinding, makeVarFilterModify, varFilterDisjunction) import Swish.RDF.BuiltIn.Datatypes (findRDFDatatype) import Swish.RDF.Proof (makeRdfSubgraphEntailmentRule , makeRdfSimpleEntailmentRule ) import Swish.RDF.Ruleset ( RDFFormula, RDFRule, RDFRuleset , makeRDFFormula , makeN3ClosureRule , makeN3ClosureSimpleRule , makeN3ClosureModifyRule , makeN3ClosureAllocatorRule , makeNodeAllocTo ) import Swish.RDF.VarBinding ( RDFVarBinding , RDFVarBindingModify , RDFVarBindingFilter , rdfVarBindingUriRef, rdfVarBindingBlank , rdfVarBindingLiteral , rdfVarBindingUntypedLiteral , rdfVarBindingXMLLiteral, rdfVarBindingDatatyped , rdfVarBindingMemberProp ) import Swish.RDF.Graph (RDFLabel(..), isUri) import Swish.RDF.Vocabulary ( namespaceRDFD , scopeRDF , scopeRDFS , scopeRDFD ) import Data.Monoid (Monoid(..)) import qualified Data.Text.Lazy.Builder as B ------------------------------------------------------------ -- Define query binding filter auxiliaries ------------------------------------------------------------ makeFormula :: Namespace -> LName -> B.Builder -> RDFFormula makeFormula = makeRDFFormula requireAny :: [RDFVarBindingFilter] -> RDFVarBindingFilter requireAny = varFilterDisjunction isLiteralV :: String -> RDFVarBindingFilter isLiteralV = rdfVarBindingLiteral . Var isUntypedLitV :: String -> RDFVarBindingFilter isUntypedLitV = rdfVarBindingUntypedLiteral . Var isXMLLitV :: String -> RDFVarBindingFilter isXMLLitV = rdfVarBindingXMLLiteral . Var isUriRefV :: String -> RDFVarBindingFilter isUriRefV = rdfVarBindingUriRef . Var isBlankV :: String -> RDFVarBindingFilter isBlankV = rdfVarBindingBlank . Var isDatatypedV :: String -> String -> RDFVarBindingFilter isDatatypedV d l = rdfVarBindingDatatyped (Var d) (Var l) isMemberPropV :: String -> RDFVarBindingFilter isMemberPropV = rdfVarBindingMemberProp . Var allocateTo :: String -> String -> [RDFLabel] -> RDFVarBindingModify allocateTo bv av = makeNodeAllocTo (Var bv) (Var av) -- Create new binding for datatype valueSame :: String -> String -> String -> String -> RDFVarBindingModify valueSame val1 typ1 val2 typ2 = sameDatatypedValue (Var val1) (Var typ1) (Var val2) (Var typ2) -- Variable binding modifier to create new binding to a canonical -- form of a datatyped literal. sameDatatypedValue :: RDFLabel -> RDFLabel -> RDFLabel -> RDFLabel -> RDFVarBindingModify sameDatatypedValue val1 typ1 val2 typ2 = VarBindingModify { vbmName = makeNSScopedName namespaceRDFD "sameValue" , vbmApply = sameDatatypedValueApplyAll val1 typ1 val2 typ2 , vbmVocab = [val1,typ1,val2,typ2] , vbmUsage = [[val2]] } sameDatatypedValueApplyAll :: RDFLabel -> RDFLabel -> RDFLabel -> RDFLabel -> [RDFVarBinding] -> [RDFVarBinding] sameDatatypedValueApplyAll val1 typ1 val2 typ2 = concatMap (sameDatatypedValueApply val1 typ1 val2 typ2) -- Auxiliary function that handles variable binding updates -- for sameDatatypedValue sameDatatypedValueApply :: RDFLabel -> RDFLabel -> RDFLabel -> RDFLabel -> RDFVarBinding -> [RDFVarBinding] sameDatatypedValueApply val1 typ1 val2 typ2 vbind = result where v1 = applyVarBinding vbind val1 t1 = applyVarBinding vbind typ1 t2 = applyVarBinding vbind typ2 sametype = getCanonical v1 t1 t2 result = if isUri t1 && isUri t2 then if t1 == t2 then case sametype of Just st -> [addVarBinding val2 st vbind] _ -> [] else error "subtype conversions not yet defined" else [] {- getCanonical :: RDFLabel -> RDFLabel -> RDFLabel -> Maybe RDFLabel getCanonical v1 t1 t2 = if isDatatyped dqn1 v1 && isJust mdt1 then liftM mkLit $ typeMkCanonicalForm dt1 (getLiteralText v1) else Nothing where dqn1 = getRes t1 dqn2 = getRes t2 mdt1 = findRDFDatatype dqn1 dt1 = fromJust mdt1 mkLit = flip Lit (Just dqn2) getRes (Res dqnam) = dqnam getRes x = error $ "Expected a Resource, sent " ++ show x -- for -Wall -} getCanonical :: RDFLabel -> RDFLabel -> RDFLabel -> Maybe RDFLabel getCanonical (TypedLit v dt) (Res dqn1) (Res dqn2) = if dt == dqn1 then case findRDFDatatype dqn1 of Just dt1 -> flip TypedLit dqn2 `fmap` typeMkCanonicalForm dt1 v _ -> Nothing else Nothing getCanonical _ _ _ = Nothing {- -- Test data qnamint = ScopedName namespaceXSD "integer" xsdint = Res qnamint lab010 = Lit "010" (Just qnamint) can010 = getCanonical lab010 xsdint xsdint nsex = Namespace "ex" "http://example.org/" resexp = Res (ScopedName nsex "p") resexs = Res (ScopedName nsex "s") vara = Var "a" varb = Var "b" varc = Var "c" vard = Var "d" varp = Var "p" vars = Var "s" vart = Var "t" vb1 = makeVarBinding [(vara,lab010),(varb,xsdint),(vard,xsdint)] vb2 = sameDatatypedValueApply vara varb varc vard vb1 vb3 = vbmApply (sameDatatypedValue vara varb varc vard) [vb1] vb3t = vb3 == vb2 vb4 = vbmApply (valueSame "a" "b" "c" "d") [vb1] vb4t = vb4 == vb2 vb5 = vbmApply (valueSame "a" "b" "c" "b") [vb1] vb5t = vb5 == vb2 vb6 = makeVarBinding [(vars,lab010),(varp,resexp),(vara,resexs),(vard,xsdint)] vb7 = vbmApply (valueSame "s" "d" "t" "d") [vb6] vb8 = makeVarBinding [(vars,lab010),(varp,resexp),(vara,resexs),(vard,xsdint) ,(vart,fromJust can010)] vb8t = vb7 == [vb8] -- -} ------------------------------------------------------------ -- Common definitions ------------------------------------------------------------ ------------------------------------------------------------ -- Define RDF axioms ------------------------------------------------------------ -- scopeRDF = Namespace "rs-rdf" "http://id.ninebynine.org/2003/Ruleset/rdf#" -- RDF axioms (from RDF semantics document, section 3.1) -- -- (See also, container property rules below) -- rdfa1 :: RDFFormula rdfa1 = makeFormula scopeRDF "a1" "rdf:type rdf:type rdf:Property ." rdfa2 :: RDFFormula rdfa2 = makeFormula scopeRDF "a2" "rdf:subject rdf:type rdf:Property ." rdfa3 :: RDFFormula rdfa3 = makeFormula scopeRDF "a3" "rdf:predicate rdf:type rdf:Property ." rdfa4 :: RDFFormula rdfa4 = makeFormula scopeRDF "a4" "rdf:object rdf:type rdf:Property ." rdfa5 :: RDFFormula rdfa5 = makeFormula scopeRDF "a5" "rdf:first rdf:type rdf:Property ." rdfa6 :: RDFFormula rdfa6 = makeFormula scopeRDF "a6" "rdf:rest rdf:type rdf:Property ." rdfa7 :: RDFFormula rdfa7 = makeFormula scopeRDF "a7" "rdf:value rdf:type rdf:Property ." rdfa8 :: RDFFormula rdfa8 = makeFormula scopeRDF "a8" "rdf:nil rdf:type rdf:List ." axiomsRDF :: [RDFFormula] axiomsRDF = [ rdfa1, rdfa2, rdfa3, rdfa4, rdfa5 , rdfa6, rdfa7, rdfa8 ] ------------------------------------------------------------ -- Define RDF rules ------------------------------------------------------------ -- RDF subgraph entailment (from RDF semantics document section 2) -- rdfsub :: RDFRule rdfsub = makeRdfSubgraphEntailmentRule (makeNSScopedName scopeRDF "sub") -- RDF simple entailment (from RDF semantics document section 7.1) -- (Note: rules se1 and se2 are combined here, because the scope of -- the "allocatedTo" modifier is the application of a single rule.) -- rdfse :: RDFRule rdfse = makeRdfSimpleEntailmentRule (makeNSScopedName scopeRDF "se") -- RDF bnode-for-literal assignments (from RDF semantics document section 7.1) -- rdflg :: RDFRule rdflg = makeN3ClosureAllocatorRule scopeRDF "lg" "?x ?a ?l . " "?x ?a ?b . ?b rdf:_allocatedTo ?l ." (makeVarFilterModify $ isLiteralV "l") (allocateTo "b" "l") -- RDF bnode-for-literal back-tracking (from RDF semantics document section 7.1) -- rdfgl :: RDFRule rdfgl = makeN3ClosureSimpleRule scopeRDF "gl" "?x ?a ?l . ?b rdf:_allocatedTo ?l . " "?x ?a ?b ." -- RDF entailment rules (from RDF semantics document section 7.2) -- -- (Note, statements with property rdf:_allocatedTo are introduced to -- track bnodes introduced according to rule rdflf [presumably this -- is actually rdflg?]) -- rdfr1 :: RDFRule rdfr1 = makeN3ClosureSimpleRule scopeRDF "r1" "?x ?a ?y ." "?a rdf:type rdf:Property ." rdfr2 :: RDFRule rdfr2 = makeN3ClosureRule scopeRDF "r2" "?x ?a ?b . ?b rdf:_allocatedTo ?l . " "?b rdf:type rdf:XMLLiteral ." (makeVarFilterModify $ isXMLLitV "l") -- Container property axioms (from RDF semantics document section 3.1) -- -- (Using here an inference rule with a filter in place of an axiom schema) -- -- This is a restricted form of the given axioms, in that the axioms -- are asserted only for container membership terms that appear in -- the graph. -- -- (This may be very inefficient for forward chaining when dealing with -- large graphs: may need to look at query logic to see if the search for -- container membership properties can be optimized. This may call for a -- custom inference rule.) -- rdfcp1 :: RDFRule rdfcp1 = makeN3ClosureRule scopeRDF "cp1" "?x ?c ?y . " "?c rdf:type rdf:Property ." (makeVarFilterModify $ isMemberPropV "c") rdfcp2 :: RDFRule rdfcp2 = makeN3ClosureRule scopeRDF "cp2" "?c ?p ?y . " "?c rdf:type rdf:Property ." (makeVarFilterModify $ isMemberPropV "c") rdfcp3 :: RDFRule rdfcp3 = makeN3ClosureRule scopeRDF "cp3" "?x ?p ?c . " "?c rdf:type rdf:Property ." (makeVarFilterModify $ isMemberPropV "c") -- Collect RDF rules -- rulesRDF :: [RDFRule] rulesRDF = [ rdfsub, rdfse , rdflg, rdfgl , rdfr1, rdfr2 , rdfcp1, rdfcp2, rdfcp3 ] -- | Ruleset for RDF inference. rulesetRDF :: RDFRuleset rulesetRDF = makeRuleset scopeRDF axiomsRDF rulesRDF ------------------------------------------------------------ -- Define RDFS axioms ------------------------------------------------------------ -- scopeRDFS = Namespace "rdfs" "http://id.ninebynine.org/2003/Ruleset/rdfs#" -- RDFS axioms (from RDF semantics document, section 4.1) -- -- (See also, container property rules below) -- rdfsa01 :: RDFFormula rdfsa01 = makeFormula scopeRDFS "a01" "rdf:type rdfs:domain rdfs:Resource ." rdfsa02 :: RDFFormula rdfsa02 = makeFormula scopeRDFS "a02" "rdf:type rdfs:range rdfs:Class ." rdfsa03 :: RDFFormula rdfsa03 = makeFormula scopeRDFS "a03" "rdfs:domain rdfs:domain rdf:Property ." rdfsa04 :: RDFFormula rdfsa04 = makeFormula scopeRDFS "a04" "rdfs:domain rdfs:range rdfs:Class ." rdfsa05 :: RDFFormula rdfsa05 = makeFormula scopeRDFS "a05" "rdfs:range rdfs:domain rdf:Property ." rdfsa06 :: RDFFormula rdfsa06 = makeFormula scopeRDFS "a06" "rdfs:range rdfs:range rdfs:Class ." rdfsa07 :: RDFFormula rdfsa07 = makeFormula scopeRDFS "a07" "rdfs:subPropertyOf rdfs:domain rdf:Property ." rdfsa08 :: RDFFormula rdfsa08 = makeFormula scopeRDFS "a08" "rdfs:subPropertyOf rdfs:range rdf:Property ." rdfsa09 :: RDFFormula rdfsa09 = makeFormula scopeRDFS "a09" "rdfs:subClassOf rdfs:domain rdfs:Class ." rdfsa10 :: RDFFormula rdfsa10 = makeFormula scopeRDFS "a10" "rdfs:subClassOf rdfs:range rdfs:Class ." rdfsa11 :: RDFFormula rdfsa11 = makeFormula scopeRDFS "a11" "rdf:subject rdfs:domain rdf:Statement ." rdfsa12 :: RDFFormula rdfsa12 = makeFormula scopeRDFS "a12" "rdf:subject rdfs:range rdfs:Resource ." rdfsa13 :: RDFFormula rdfsa13 = makeFormula scopeRDFS "a13" "rdf:predicate rdfs:domain rdf:Statement ." rdfsa14 :: RDFFormula rdfsa14 = makeFormula scopeRDFS "a14" "rdf:predicate rdfs:range rdfs:Resource ." rdfsa15 :: RDFFormula rdfsa15 = makeFormula scopeRDFS "a15" "rdf:object rdfs:domain rdf:Statement ." rdfsa16 :: RDFFormula rdfsa16 = makeFormula scopeRDFS "a16" "rdf:object rdfs:range rdfs:Resource ." rdfsa17 :: RDFFormula rdfsa17 = makeFormula scopeRDFS "a17" "rdfs:member rdfs:domain rdfs:Resource ." rdfsa18 :: RDFFormula rdfsa18 = makeFormula scopeRDFS "a18" "rdfs:member rdfs:range rdfs:Resource ." rdfsa19 :: RDFFormula rdfsa19 = makeFormula scopeRDFS "a19" "rdf:first rdfs:domain rdf:List ." rdfsa20 :: RDFFormula rdfsa20 = makeFormula scopeRDFS "a20" "rdf:first rdfs:range rdfs:Resource ." rdfsa21 :: RDFFormula rdfsa21 = makeFormula scopeRDFS "a21" "rdf:rest rdfs:domain rdf:List ." rdfsa22 :: RDFFormula rdfsa22 = makeFormula scopeRDFS "a22" "rdf:rest rdfs:range rdf:List ." rdfsa23 :: RDFFormula rdfsa23 = makeFormula scopeRDFS "a23" "rdfs:seeAlso rdfs:domain rdfs:Resource ." rdfsa24 :: RDFFormula rdfsa24 = makeFormula scopeRDFS "a24" "rdfs:seeAlso rdfs:range rdfs:Resource ." rdfsa25 :: RDFFormula rdfsa25 = makeFormula scopeRDFS "a25" "rdfs:isDefinedBy rdfs:domain rdfs:Resource ." rdfsa26 :: RDFFormula rdfsa26 = makeFormula scopeRDFS "a26" "rdfs:isDefinedBy rdfs:range rdfs:Resource ." rdfsa27 :: RDFFormula rdfsa27 = makeFormula scopeRDFS "a27" "rdfs:isDefinedBy rdfs:subPropertyOf rdfs:seeAlso ." rdfsa28 :: RDFFormula rdfsa28 = makeFormula scopeRDFS "a28" "rdfs:comment rdfs:domain rdfs:Resource ." rdfsa29 :: RDFFormula rdfsa29 = makeFormula scopeRDFS "a29" "rdfs:comment rdfs:range rdfs:Literal ." rdfsa30 :: RDFFormula rdfsa30 = makeFormula scopeRDFS "a30" "rdfs:label rdfs:domain rdfs:Resource ." rdfsa31 :: RDFFormula rdfsa31 = makeFormula scopeRDFS "a31" "rdfs:label rdfs:range rdfs:Literal ." rdfsa32 :: RDFFormula rdfsa32 = makeFormula scopeRDFS "a32" "rdf:value rdfs:domain rdfs:Resource ." rdfsa33 :: RDFFormula rdfsa33 = makeFormula scopeRDFS "a33" "rdf:value rdfs:range rdfs:Resource ." rdfsa34 :: RDFFormula rdfsa34 = makeFormula scopeRDFS "a34" "rdf:Alt rdfs:subClassOf rdfs:Container ." rdfsa35 :: RDFFormula rdfsa35 = makeFormula scopeRDFS "a35" "rdf:Bag rdfs:subClassOf rdfs:Container ." rdfsa36 :: RDFFormula rdfsa36 = makeFormula scopeRDFS "a36" "rdf:Seq rdfs:subClassOf rdfs:Container ." rdfsa37 :: RDFFormula rdfsa37 = makeFormula scopeRDFS "a37" "rdfs:ContainerMembershipProperty rdfs:subClassOf rdf:Property ." rdfsa38 :: RDFFormula rdfsa38 = makeFormula scopeRDFS "a38" "rdf:XMLLiteral rdf:type rdfs:Datatype ." rdfsa39 :: RDFFormula rdfsa39 = makeFormula scopeRDFS "a39" "rdf:XMLLiteral rdfs:subClassOf rdfs:Literal ." rdfsa40 :: RDFFormula rdfsa40 = makeFormula scopeRDFS "a40" "rdfs:Datatype rdfs:subClassOf rdfs:Class ." axiomsRDFS :: [RDFFormula] axiomsRDFS = [ rdfsa01, rdfsa02, rdfsa03, rdfsa04 , rdfsa05, rdfsa06, rdfsa07, rdfsa08, rdfsa09 , rdfsa10, rdfsa11, rdfsa12, rdfsa13, rdfsa14 , rdfsa15, rdfsa16, rdfsa17, rdfsa18, rdfsa19 , rdfsa20, rdfsa21, rdfsa22, rdfsa23, rdfsa24 , rdfsa25, rdfsa26, rdfsa27, rdfsa28, rdfsa29 , rdfsa30, rdfsa31, rdfsa32, rdfsa33, rdfsa34 , rdfsa35, rdfsa36, rdfsa37, rdfsa38, rdfsa39 , rdfsa40 ] ------------------------------------------------------------ -- Define RDFS rules ------------------------------------------------------------ {- rdfr2 = makeN3ClosureRule scopeRDF "r2" "?x ?a ?b . ?b rdf:_allocatedTo ?l . " "?b rdf:type rdf:XMLLiteral ." (makeVarFilterModify $ isXMLLit "?l") -} -- RDFS entailment rules (from RDF semantics document section 7.2) -- -- (Note, statements with property rdf:_allocatedTo are introduced to -- track bnodes introduced according to rule rdflf [presumably this -- is actually rdflg?]) -- rdfsr1 :: RDFRule rdfsr1 = makeN3ClosureRule scopeRDFS "r1" "?x ?a ?b . ?b rdf:_allocatedTo ?l . " "?b rdf:type rdfs:Literal ." (makeVarFilterModify $ isUntypedLitV "l" ) rdfsr2 :: RDFRule rdfsr2 = makeN3ClosureSimpleRule scopeRDFS "r2" "?x ?a ?y . ?a rdfs:domain ?z ." "?x rdf:type ?z ." rdfsr3 :: RDFRule rdfsr3 = makeN3ClosureRule scopeRDFS "r3" "?u ?a ?v . ?a rdfs:range ?z ." "?v rdf:type ?z ." (makeVarFilterModify $ requireAny [isUriRefV "v",isBlankV "v"]) rdfsr4a :: RDFRule rdfsr4a = makeN3ClosureSimpleRule scopeRDFS "r4a" "?x ?a ?y ." "?x rdf:type rdfs:Resource ." rdfsr4b :: RDFRule rdfsr4b = makeN3ClosureRule scopeRDFS "r4b" "?x ?a ?u ." "?u rdf:type rdfs:Resource ." (makeVarFilterModify $ requireAny [isUriRefV "u",isBlankV "u"]) rdfsr5 :: RDFRule rdfsr5 = makeN3ClosureSimpleRule scopeRDFS "r5" "?a rdfs:subPropertyOf ?b . ?b rdfs:subPropertyOf ?c ." "?a rdfs:subPropertyOf ?c ." rdfsr6 :: RDFRule rdfsr6 = makeN3ClosureSimpleRule scopeRDFS "r6" "?x rdf:type rdf:Property ." "?x rdfs:subPropertyOf ?x ." rdfsr7 :: RDFRule rdfsr7 = makeN3ClosureSimpleRule scopeRDFS "r7" "?x ?a ?y . ?a rdfs:subPropertyOf ?b ." "?x ?b ?y ." rdfsr8 :: RDFRule rdfsr8 = makeN3ClosureSimpleRule scopeRDFS "r8" "?x rdf:type rdfs:Class ." "?x rdfs:subClassOf rdfs:Resource ." rdfsr9 :: RDFRule rdfsr9 = makeN3ClosureSimpleRule scopeRDFS "r9" "?x rdfs:subClassOf ?y . ?a rdf:type ?x ." "?a rdf:type ?y ." rdfsr10 :: RDFRule rdfsr10 = makeN3ClosureSimpleRule scopeRDFS "r10" "?x rdf:type rdfs:Class ." "?x rdfs:subClassOf ?x ." rdfsr11 :: RDFRule rdfsr11 = makeN3ClosureSimpleRule scopeRDFS "r11" "?x rdfs:subClassOf ?y . ?y rdfs:subClassOf ?z ." "?x rdfs:subClassOf ?z ." rdfsr12 :: RDFRule rdfsr12 = makeN3ClosureSimpleRule scopeRDFS "r12" "?x rdf:type rdfs:ContainerMembershipProperty ." "?x rdfs:subPropertyOf rdfs:member ." rdfsr13 :: RDFRule rdfsr13 = makeN3ClosureSimpleRule scopeRDFS "r13" "?x rdf:type rdfs:Datatype ." "?x rdfs:subClassOf rdfs:Literal ." -- These are valid only under an extensional strengthening of RDFS, -- discussed in section 7.3.1 of the RDF semantics specification: {- rdfsrext1 :: RDFRule rdfsrext1 = makeN3ClosureSimpleRule scopeRDFS "ext1" "?x rdfs:domain ?y . ?y rdfs:subClassOf ?z ." "?x rdfs:domain ?z ." rdfsrext2 :: RDFRule rdfsrext2 = makeN3ClosureSimpleRule scopeRDFS "ext2" "?x rdfs:range ?y . ?y rdfs:subClassOf ?z ." "?x rdfs:range ?z ." rdfsrext3 :: RDFRule rdfsrext3 = makeN3ClosureSimpleRule scopeRDFS "ext3" "?x rdfs:domain ?y . ?z rdfs:subPropertyOf ?x ." "?z rdfs:domain ?y ." rdfsrext4 :: RDFRule rdfsrext4 = makeN3ClosureSimpleRule scopeRDFS "ext4" "?x rdfs:range ?y . ?z rdfs:subPropertyOf ?x ." "?z rdfs:range ?y ." rdfsrext5 :: RDFRule rdfsrext5 = makeN3ClosureSimpleRule scopeRDFS "ext5" "rdf:type rdfs:subPropertyOf ?z . ?z rdfs:domain ?y ." "rdfs:Resource rdfs:subClassOf ?y ." rdfsrext6 :: RDFRule rdfsrext6 = makeN3ClosureSimpleRule scopeRDFS "rext6" "rdfs:subClassOf rdfs:subPropertyOf ?z . ?z rdfs:domain ?y ." "rdfs:Class rdfs:subClassOf ?y ." rdfsrext7 :: RDFRule rdfsrext7 = makeN3ClosureSimpleRule scopeRDFS "rext7" "rdfs:subPropertyOf rdfs:subPropertyOf ?z . ?z rdfs:domain ?y ." "rdfs:Property rdfs:subClassOf ?y ." rdfsrext8 :: RDFRule rdfsrext8 = makeN3ClosureSimpleRule scopeRDFS "rext8" "rdfs:subClassOf rdfs:subPropertyOf ?z . ?z rdfs:range ?y ." "rdfs:Class rdfs:subClassOf ?y ." rdfsrext9 :: RDFRule rdfsrext9 = makeN3ClosureSimpleRule scopeRDFS "rext9" "rdfs:subPropertyOf rdfs:subPropertyOf ?z . ?z rdfs:range ?y ." "rdfs:Property rdfs:subClassOf ?y ." -} -- Container property axioms (from RDF semantics document section 4.1) -- -- (Using here an inference rule with a filter in place of an axiom schema) -- -- This is a restricted form of the given axioms, in that the axioms -- are asserted only for container membership terms that appear in -- the graph. -- -- (This may be very inefficient for forward chaining when dealing with -- large graphs: may need to look at query logic to see if the search for -- container membership properties can be optimized. This may call for a -- custom inference rule.) -- rdfscp11 :: RDFRule rdfscp11 = makeN3ClosureRule scopeRDFS "cp11" "?x ?c ?y . " "?c rdf:type rdfs:ContainerMembershipProperty ." (makeVarFilterModify $ isMemberPropV "c") rdfscp12 :: RDFRule rdfscp12 = makeN3ClosureRule scopeRDFS "cp12" "?c ?p ?y . " "?c rdf:type rdfs:ContainerMembershipProperty ." (makeVarFilterModify $ isMemberPropV "c") rdfscp13 :: RDFRule rdfscp13 = makeN3ClosureRule scopeRDFS "cp13" "?x ?p ?c . " "?c rdf:type rdfs:ContainerMembershipProperty ." (makeVarFilterModify $ isMemberPropV "c") rdfscp21 :: RDFRule rdfscp21 = makeN3ClosureRule scopeRDFS "cp21" "?x ?c ?y . " "?c rdfs:domain rdfs:Resource ." (makeVarFilterModify $ isMemberPropV "c") rdfscp22 :: RDFRule rdfscp22 = makeN3ClosureRule scopeRDFS "cp22" "?c ?p ?y . " "?c rdfs:domain rdfs:Resource ." (makeVarFilterModify $ isMemberPropV "c") rdfscp23 :: RDFRule rdfscp23 = makeN3ClosureRule scopeRDFS "cp23" "?x ?p ?c . " "?c rdfs:domain rdfs:Resource ." (makeVarFilterModify $ isMemberPropV "c") rdfscp31 :: RDFRule rdfscp31 = makeN3ClosureRule scopeRDFS "cp31" "?x ?c ?y . " "?c rdfs:range rdfs:Resource ." (makeVarFilterModify $ isMemberPropV "c") rdfscp32 :: RDFRule rdfscp32 = makeN3ClosureRule scopeRDFS "cp32" "?c ?p ?y . " "?c rdfs:range rdfs:Resource ." (makeVarFilterModify $ isMemberPropV "c") rdfscp33 :: RDFRule rdfscp33 = makeN3ClosureRule scopeRDFS "cp33" "?x ?p ?c . " "?c rdfs:range rdfs:Resource ." (makeVarFilterModify $ isMemberPropV "c") -- Collect RDFS rules -- rulesRDFS :: [RDFRule] rulesRDFS = [ rdfsr1, rdfsr2, rdfsr3, rdfsr4a, rdfsr4b , rdfsr5, rdfsr6, rdfsr7, rdfsr8, rdfsr9 , rdfsr10, rdfsr11, rdfsr12, rdfsr13 , rdfscp11, rdfscp12, rdfscp13 , rdfscp21, rdfscp22, rdfscp23 , rdfscp31, rdfscp32, rdfscp33 ] -- | Ruleset for RDFS inference. rulesetRDFS :: RDFRuleset rulesetRDFS = makeRuleset scopeRDFS axiomsRDFS rulesRDFS ------------------------------------------------------------ -- Define RDFD (datatyping) axioms ------------------------------------------------------------ -- scopeRDFD = Namespace "rdfd" "http://id.ninebynine.org/2003/Ruleset/rdfd#" axiomsRDFD :: [RDFFormula] axiomsRDFD = [ ] ------------------------------------------------------------ -- Define RDFD (datatyping) axioms ------------------------------------------------------------ -- RDFD closure rules from semantics document, section 7.4 -- Infer type of datatyped literal -- rdfdr1 :: RDFRule rdfdr1 = makeN3ClosureRule scopeRDFD "r1" "?d rdf:type rdfs:Datatype . ?a ?p ?l . ?b rdf:_allocatedTo ?l . " "?b rdf:type ?d ." (makeVarFilterModify $ isDatatypedV "d" "l") -- Equivalent literals with same datatype: -- (generate canonical form, or operate in proof mode only) -- rdfdr2 :: RDFRule rdfdr2 = makeN3ClosureRule scopeRDFD "r2" "?d rdf:type rdfs:Datatype . ?a ?p ?s ." "?a ?p ?t ." (valueSame "s" "d" "t" "d") {- Note that valueSame does datatype check. Otherwise use: rdfdr2 = makeN3ClosureModifyRule scopeRDFD "r2" "?d rdf:type rdfs:Datatype . ?a ?p ?s ." "?a ?p ?t ." (makeVarFilterModify $ isDatatypedV "d" "s") (valueSame "s" "d" "t" "d") -} -- Equivalent literals with different datatypes: -- (generate canonical form, or operate in proof mode only) -- rdfdr3 :: RDFRule rdfdr3 = makeN3ClosureModifyRule scopeRDFD "r3" ( "?d rdf:type rdfs:Datatype . ?e rdf:type rdfs:Datatype . " `mappend` "?a ?p ?s ." ) "?a ?p ?t ." (makeVarFilterModify $ isDatatypedV "s" "d") (valueSame "s" "d" "t" "e") -- Collect RDFD rules -- rulesRDFD :: [RDFRule] rulesRDFD = [ rdfdr1, rdfdr2, rdfdr3 ] -- | Ruleset for RDFD (datatyping) inference. -- rulesetRDFD :: RDFRuleset rulesetRDFD = makeRuleset scopeRDFD axiomsRDFD rulesRDFD -------------------------------------------------------------------------------- -- -- Copyright (c) 2003, Graham Klyne, 2009 Vasili I Galchin, -- 2011, 2012 Douglas Burke -- All rights reserved. -- -- This file is part of Swish. -- -- Swish is free software; you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation; either version 2 of the License, or -- (at your option) any later version. -- -- Swish is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with Swish; if not, write to: -- The Free Software Foundation, Inc., -- 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -- --------------------------------------------------------------------------------