Copyright | (c) 2003 Graham Klyne 2009 Vasili I Galchin 2011 2012 2022 Douglas Burke |
---|---|
License | GPL V2 |
Maintainer | Douglas Burke |
Stability | experimental |
Portability | CPP, DerivingStrategies, OverloadedStrings |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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
Show ex => Show (Formula ex) Source # | |
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 |
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