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.
- 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.
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 | |
|
type RuleMap ex = Map ScopedName (Rule ex) Source
A set of rules labelled with their name.
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
:: 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 -> ShowS Source
Show a string left justified in a field of at least the specified number of characters width.