Portability  MultiParamTypeClasses, OverloadedStrings 

Stability  experimental 
Maintainer  Douglas 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 where
 data Formula ex = Formula {
 formName :: ScopedName
 formExpr :: ex
 data Rule ex = Rule {
 ruleName :: ScopedName
 fwdApply :: [ex] > [ex]
 bwdApply :: ex > [[ex]]
 checkInference :: [ex] > ex > Bool
 type RuleMap ex = LookupMap (Rule ex)
 nullScope :: Namespace
 nullSN :: Text > ScopedName
 nullFormula :: Formula ex
 nullRule :: Rule ex
 fwdCheckInference :: Eq ex => Rule ex > [ex] > ex > Bool
 bwdCheckInference :: Eq ex => Rule ex > [ex] > ex > Bool
 showsFormula :: ShowM ex => String > Formula ex > ShowS
 showsFormulae :: ShowM ex => String > [Formula ex] > String > ShowS
 showsWidth :: Int > String > ShowS
Documentation
class Eq ex => Expression ex whereSource
Expression is a type class for values over which proofs may be constructed.
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 
A Formula is a named expression.
Formula  

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

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) 
nullSN :: Text > ScopedNameSource
nullFormula :: Formula exSource
The null formula.
Checks that consequence is a result of applying the rule to the antecedants.
Create a displayable form of a labelled formula
:: ShowM 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 > ShowSSource
Show a string left justified in a field of at least the specified number of characters width.