Swish.Rule

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.

Documentation

class Eq ex => Expression ex where

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

Methods

isValid :: ex -> Bool

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

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

Defined in Swish.RDF.Proof

Methods

isValid :: lg lb -> Bool

data Formula ex

A Formula is a named expression.

Constructors

Formula

Fields

• formName :: ScopedName

  Name used for formula in proof chain

• formExpr :: ex

  Named formula value

Instances

Eq (Formula ex)

Define equality of formulae as equality of formula names

Defined in Swish.Rule

Methods

(==) :: Formula ex -> Formula ex -> Bool

(/=) :: Formula ex -> Formula ex -> Bool

Ord (Formula ex)

Define ordering of formulae based on formula names

Defined in Swish.Rule

Methods

compare :: Formula ex -> Formula ex -> Ordering

(<) :: Formula ex -> Formula ex -> Bool

(<=) :: Formula ex -> Formula ex -> Bool

(>) :: Formula ex -> Formula ex -> Bool

(>=) :: Formula ex -> Formula ex -> Bool

max :: Formula ex -> Formula ex -> Formula ex

min :: Formula ex -> Formula ex -> Formula ex

Show ex => Show (Formula ex)

Defined in Swish.Rule

Methods

showsPrec :: Int -> Formula ex -> ShowS

show :: Formula ex -> String

showList :: [Formula ex] -> ShowS

data Rule ex

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

Constructors

Rule

Fields

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

Instances

Eq (Rule ex)

Define equality of rules as equality of the rule names.

Defined in Swish.Rule

Methods

(==) :: Rule ex -> Rule ex -> Bool

(/=) :: Rule ex -> Rule ex -> Bool

Ord (Rule ex)

Define ordering of rules based on the rule names.

Defined in Swish.Rule

Methods

compare :: Rule ex -> Rule ex -> Ordering

(<) :: Rule ex -> Rule ex -> Bool

(<=) :: Rule ex -> Rule ex -> Bool

(>) :: Rule ex -> Rule ex -> Bool

(>=) :: Rule ex -> Rule ex -> Bool

max :: Rule ex -> Rule ex -> Rule ex

min :: Rule ex -> Rule ex -> Rule ex

Show (Rule ex)

Defined in Swish.Rule

Methods

showsPrec :: Int -> Rule ex -> ShowS

show :: Rule ex -> String

showList :: [Rule ex] -> ShowS

type RuleMap ex = Map ScopedName (Rule ex)

A set of rules labelled with their name.

nullScope :: Namespace

The namespace http://id.ninebynine.org/2003/Ruleset/null with the prefix null:.

nullSN

Arguments

:: LName

local name.

-> ScopedName

Create a scoped name with the null namespace.

nullFormula :: Formula ex

The null formula.

nullRule :: Rule ex

The null rule.

fwdCheckInference

Arguments

:: Eq ex

=> Rule ex

rule

-> [ex]

antecedants

-> ex

consequence

-> Bool

Checks that consequence is a result of applying the rule to the antecedants.

bwdCheckInference

Arguments

:: Eq ex

=> Rule ex

rule

-> [ex]

antecedants

-> ex

consequence

-> Bool

Checks that the antecedants are all required to create the consequence using the given rule.

showsFormula

Arguments

:: ShowLines ex

=> String

newline

-> Formula ex

formula

-> ShowS

Create a displayable form of a labelled formula

showsFormulae

Arguments

:: ShowLines ex

=> String

newline

-> [Formula ex]

the formulae to show

-> String

text to be placed after the formulae

-> ShowS

Return a displayable form of a list of labelled formulae

showsWidth :: Int -> String -> ShowS

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