Portability  MultiParamTypeClasses, OverloadedStrings 

Stability  experimental 
Maintainer  Douglas Burke 
Safe Haskell  SafeInfered 
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 :: LName > ScopedName
 nullFormula :: Formula ex
 nullRule :: Rule ex
 fwdCheckInference :: Eq ex => Rule ex > [ex] > ex > Bool
 bwdCheckInference :: Eq ex => Rule ex > [ex] > ex > Bool
 showsFormula :: ShowLines ex => String > Formula ex > ShowS
 showsFormulae :: ShowLines 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 the rule names. 
Ord (Rule ex)  Define ordering of rules based on the rule names. 
Show (Rule ex)  
LookupEntryClass (Rule ex) ScopedName (Rule ex) 
The namespace http://id.ninebynine.org/2003/Ruleset/null
with the prefix null:
.
nullFormula :: Formula exSource
The null formula.
Checks that consequence is a result of applying the rule to the antecedants.
Checks that the antecedants are all required to create the consequence using the given rule.
Create a displayable form of a labelled formula
:: 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 > ShowSSource
Show a string left justified in a field of at least the specified number of characters width.