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.