Copyright  (c) 2003 Graham Klyne 2009 Vasili I Galchin 2011 2012 Douglas Burke 

License  GPL V2 
Maintainer  Douglas Burke 
Stability  experimental 
Portability  OverloadedStrings 
Safe Haskell  None 
Language  Haskell98 
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.
Synopsis
 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 = Map ScopedName (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 where Source #
Expression is a type class for values over which proofs may be constructed.
isValid :: ex > Bool Source #
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) Source #  Instances of 
Defined in Swish.RDF.Proof 
A Formula is a named expression.
Formula  

Instances
Eq (Formula ex) Source #  Define equality of formulae as equality of formula names 
Ord (Formula ex) Source #  Define ordering of formulae based on formula names 
Show ex => Show (Formula ex) Source #  
Rule is a data type for inference rules that can be used to construct a step in a proof.
Rule  

nullScope :: Namespace Source #
The namespace http://id.ninebynine.org/2003/Ruleset/null
with the prefix null:
.
nullFormula :: Formula ex Source #
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