Portability  MultiParamTypeClasses 

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
 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) 
nullFormula :: Formula exSource
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.