Portability | FlexibleInstances, UndecidableInstances |
---|---|

Stability | experimental |

Maintainer | Douglas Burke |

This module instantiates the `Proof`

framework for
constructing proofs over RDFGraph expressions.
The intent is that this can be used to test some
correspondences between the RDF Model theory and
corresponding proof theory based on closure rules
applied to the graph, per http://www.w3.org/TR/rdf-mt/.

- type RDFProof = Proof RDFGraph
- type RDFProofStep = Step RDFGraph
- makeRDFProof :: [RDFRuleset] -> RDFFormula -> RDFFormula -> [RDFProofStep] -> RDFProof
- makeRDFProofStep :: RDFRule -> [RDFFormula] -> RDFFormula -> RDFProofStep
- makeRdfInstanceEntailmentRule :: ScopedName -> [RDFLabel] -> RDFRule
- makeRdfSubgraphEntailmentRule :: ScopedName -> RDFRule
- makeRdfSimpleEntailmentRule :: ScopedName -> RDFRule

# Documentation

type RDFProofStep = Step RDFGraphSource

:: [RDFRuleset] | RDF rulesets that constitute a proof context for this proof |

-> RDFFormula | initial statement from which the goal is claimed to be proven |

-> RDFFormula | statement that is claimed to be proven |

-> [RDFProofStep] | |

-> RDFProof |

Make an RDF proof

:: RDFRule | rule to use for this step |

-> [RDFFormula] | antecedent RDF formulae for this step |

-> RDFFormula | RDF formula that is the consequent for this step |

-> RDFProofStep |

Make an RDF graph proof step

makeRdfInstanceEntailmentRuleSource

:: ScopedName | name |

-> [RDFLabel] | vocabulary |

-> RDFRule |

Make an inference rule dealing with RDF instance entailment; i.e. entailments that are due to replacement of a URI or literal node with a blank node.

The part of this rule expected to be useful is `checkInference`

.
The `fwdApply`

and `bwdApply`

functions defined here may return
rather large results if applied to graphs with many variables or
a large vocabulary, and are defined for experimentation.

Forward and backward chaining is performed with respect to a
specified vocabulary. In the case of backward chaining, it would
otherwise be impossible to bound the options thus generated.
In the case of forward chaining, it is often not desirable to
have the properties generalized. If forward or backward backward
chaining will not be used, supply an empty vocabulary.
Note: graph method `allNodes`

can be used to obtain a list of all
the subjects and objuects used ina graph, not counting nested
formulae; use a call of the form:

allNodes (not . labelIsVar) graph

makeRdfSubgraphEntailmentRule :: ScopedName -> RDFRuleSource

Make an inference rule dealing with RDF subgraph entailment.
The part of this rule expected to be useful is `checkInference`

.
The `fwdApply`

function defined here may return rather large
results. But in the name of completeness and experimentation
with the possibilities of lazy evaluation, it has been defined.

Backward chaining is not performed, as there is no reasonable way to choose a meaningful supergraph of that supplied.

makeRdfSimpleEntailmentRule :: ScopedName -> RDFRuleSource

Make an inference rule dealing with RDF simple entailment.
The part of this rule expected to be useful is `checkInference`

.
The `fwdApply`

and `bwdApply`

functions defined return null
results, indicating that they are not useful for the purposes
of proof discovery.