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

Swish.Rule

Description

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
- isValid :: ex -> Bool
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.

Methods

isValid :: ex -> Bool Source #

Is expression true in all interpretations? If so, then its truth is assumed without justification.

Instances

Instances details

(LDGraph lg lb, Eq (lg lb)) => Expression (lg lb) Source #	Instances of `LDGraph` are also instance of the `Expression` class, for which proofs can be constructed. The empty RDF graph is always `True` (other enduring truths are asserted as axioms).
Instance details Defined in Swish.RDF.Proof Methods isValid :: lg lb -> Bool Source #

data Formula ex Source #

A Formula is a named expression.

Constructors

Formula
Fields formName :: ScopedName Name used for formula in proof chain formExpr :: ex Named formula value

Instances

Instances details

Show ex => Show (Formula ex) Source #
Instance details Defined in Swish.Rule Methods showsPrec :: Int -> Formula ex -> ShowS # show :: Formula ex -> String # showList :: [Formula ex] -> ShowS #
Eq (Formula ex) Source #	Define equality of formulae as equality of formula names
Instance details Defined in Swish.Rule Methods (==) :: Formula ex -> Formula ex -> Bool # (/=) :: Formula ex -> Formula ex -> Bool #
Ord (Formula ex) Source #	Define ordering of formulae based on formula names
Instance details Defined in Swish.Rule Methods compare :: Formula ex -> Formula ex -> Ordering # (<) :: Formula ex -> Formula ex -> Bool # (<=) :: Formula ex -> Formula ex -> Bool # (>) :: Formula ex -> Formula ex -> Bool # (>=) :: Formula ex -> Formula ex -> Bool # max :: Formula ex -> Formula ex -> Formula ex # min :: Formula ex -> Formula ex -> Formula ex #

data Rule ex Source #

Rule is a data type for inference rules that can be used to construct a step in a proof.

Constructors

Rule

Fields

ruleName :: ScopedName
Name of rule, for use when displaying a proof
fwdApply :: [ex] -> [ex]
Forward application of a rule, takes a list of expressions and returns a list (possibly empty) of forward applications of the rule to combinations of the antecedent expressions. Note that all of the results returned can be assumed to be (simultaneously) true, given the antecedents provided.
bwdApply :: ex -> [[ex]]
Backward application of a rule, takes an expression and returns a list of alternative antecedents, each of which is a list of expressions that jointly yield the given consequence through application of the inference rule. An empty list is returned if no antecedents will allow the consequence to be inferred.
checkInference :: [ex] -> ex -> Bool
Inference check. Takes a list of antecedent expressions and a consequent expression, returning True if the consequence can be obtained from the antecedents by application of the rule. When the antecedents and consequent are both given, this is generally more efficient that using either forward or backward chaining. Also, a particular rule may not fully support either forward or backward chaining, but all rules are required to fully support this function.
A default implementation based on forward chaining is given below.

Instances

Instances details

Show (Rule ex) Source #
Instance details Defined in Swish.Rule Methods showsPrec :: Int -> Rule ex -> ShowS # show :: Rule ex -> String # showList :: [Rule ex] -> ShowS #
Eq (Rule ex) Source #	Define equality of rules as equality of the rule names.
Instance details Defined in Swish.Rule Methods (==) :: Rule ex -> Rule ex -> Bool # (/=) :: Rule ex -> Rule ex -> Bool #
Ord (Rule ex) Source #	Define ordering of rules based on the rule names.
Instance details Defined in Swish.Rule Methods compare :: Rule ex -> Rule ex -> Ordering # (<) :: Rule ex -> Rule ex -> Bool # (<=) :: Rule ex -> Rule ex -> Bool # (>) :: Rule ex -> Rule ex -> Bool # (>=) :: Rule ex -> Rule ex -> Bool # max :: Rule ex -> Rule ex -> Rule ex # min :: Rule ex -> Rule ex -> Rule ex #

type RuleMap ex = Map ScopedName (Rule ex) Source #

A set of rules labelled with their name.

nullScope :: Namespace Source #

The namespace http://id.ninebynine.org/2003/Ruleset/null with the prefix null:.

nullSN Source #

Arguments

:: LName	local name.
-> ScopedName

Create a scoped name with the null namespace.

nullFormula :: Formula ex Source #

The null formula.

nullRule :: Rule ex Source #

The null rule.

fwdCheckInference Source #

Arguments

:: Eq ex
=> Rule ex	rule
-> [ex]	antecedants
-> ex	consequence
-> Bool

Checks that consequence is a result of applying the rule to the antecedants.

bwdCheckInference Source #

Arguments

:: Eq ex
=> Rule ex	rule
-> [ex]	antecedants
-> ex	consequence
-> Bool

Checks that the antecedants are all required to create the consequence using the given rule.

showsFormula Source #

Arguments

:: ShowLines ex
=> String	newline
-> Formula ex	formula
-> ShowS

Create a displayable form of a labelled formula

showsFormulae Source #

Arguments

:: 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.