swish- A semantic web toolkit.

MaintainerDouglas Burke



This module defines a framework for defining inference rules over some expression form. It is intended to be used with RDF graphs, but the structures aim to be quite generic with respect to the expression forms allowed.



class Eq ex => Expression ex whereSource

Expression is a type class for values over which proofs may be constructed.


isValid :: ex -> BoolSource

Is expression true in all interpretations? If so, then its truth is assumed without justification.


(Label lb, LDGraph 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).

data Formula ex Source

A Formula is a named expression.




formName :: ScopedName

Name used for formula in proof chain

formExpr :: ex

Named formula value


Eq (Formula ex)

Define equality of formulae as equality of formula names

Ord (Formula ex)

Define ordering of formulae based on formula names

Show ex => Show (Formula ex) 
LookupEntryClass (Formula ex) ScopedName (Formula ex) 

data Rule ex Source

Rule is a data type for inference rules that can be used to construct a step in a proof.




ruleName :: ScopedName

Name of rule, for use when displaying a proof

fwdApply :: [ex] -> [ex]

Forward application of a rule, takes a list of expressions and returns a list (possibly empty) of forward applications of the rule to combinations of the antecedent expressions. Note that all of the results returned can be assumed to be (simultaneously) true, given the antecedents provided.

bwdApply :: ex -> [[ex]]

Backward application of a rule, takes an expression and returns a list of alternative antecedents, each of which is a list of expressions that jointly yield the given consequence through application of the inference rule. An empty list is returned if no antecedents will allow the consequence to be inferred.

checkInference :: [ex] -> ex -> Bool

Inference check. Takes a list of antecedent expressions and a consequent expression, returning True if the consequence can be obtained from the antecedents by application of the rule. When the antecedents and consequent are both given, this is generally more efficient that using either forward or backward chaining. Also, a particular rule may not fully support either forward or backward chaining, but all rules are required to fully support this function.

A default implementation based on forward chaining is given below.


Eq (Rule ex)

Define equality of rules as equality of rule names

Ord (Rule ex)

Define ordering of rules based on rule names

Show (Rule ex) 
LookupEntryClass (Rule ex) ScopedName (Rule ex) 

nullScope :: NamespaceSource

The namespace http:id.ninebynine.org2003Ruleset/null

fwdCheckInference :: Eq ex => Rule ex -> [ex] -> ex -> BoolSource

bwdCheckInference :: Eq ex => Rule ex -> [ex] -> ex -> BoolSource

showsFormula :: ShowM ex => String -> Formula ex -> ShowSSource

Create a displayable form of a labelled formula

showsFormulae :: ShowM ex => String -> [Formula ex] -> String -> ShowSSource

Return a displayable form of a list of labelled formulae

showsWidth :: Int -> String -> ShowSSource

Show a string left justified in a field of at least the specified number of characters width.