Swish.RDF.Proof

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/.

Documentation

type RDFProof = Proof RDFGraph

An RDF proof.

type RDFProofStep = Step RDFGraph

A step in an RDF proof.

makeRDFProof

Arguments

:: [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]

the chain of inference rules in the proof.

-> RDFProof

Make an RDF proof.

makeRDFProofStep

Arguments

:: 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.

makeRdfInstanceEntailmentRule

Arguments

:: 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 objects used in a graph, not counting nested formulae; use a call of the form:

 allNodes (not . labelIsVar) graph

makeRdfSubgraphEntailmentRule :: ScopedName -> RDFRule

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 -> RDFRule

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.

Orphan instances

(LDGraph lg lb, Eq (lg lb)) => Expression (lg lb)

Instances of LDGraph are also instance of the Expression class, for which proofs can be constructed. The empty RDF graph is always True (other enduring truths are asserted as axioms).

Methods

isValid :: lg lb -> Bool