swish-0.10.1.0: A semantic web toolkit.

Copyright | (c) 2003 Graham Klyne 2009 Vasili I Galchin 2011 2016 Douglas Burke
License | GPL V2
Maintainer | Douglas Burke
Stability | experimental
Portability | H98
Safe Haskell | None
Language | Haskell2010

Swish.Proof

Description

This module defines a framework for constructing proofs 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.

It does not define any proof-finding strategy.

Synopsis

- data Proof ex = Proof {
  - proofContext :: [Ruleset ex]
  - proofInput :: Formula ex
  - proofResult :: Formula ex
  - proofChain :: [Step ex]
  }
- data Step ex = Step {
  - stepRule :: Rule ex
  - stepAnt :: [Formula ex]
  - stepCon :: Formula ex
  }
- checkProof :: (Expression ex, Ord ex) => Proof ex -> Bool
- explainProof :: (Expression ex, Ord ex) => Proof ex -> Maybe String
- checkStep :: Ord ex => [Rule ex] -> [ex] -> Step ex -> Bool
- showProof :: ShowLines ex => String -> Proof ex -> String
- showsProof :: ShowLines ex => String -> Proof ex -> ShowS
- showsFormula :: ShowLines ex => String -> Formula ex -> ShowS

# Documentation

data Proof ex Source #

Proof is a structure that presents a chain of rule applications that yield a result expression from a given expression

Constructors

Proof |

Fields

- proofContext :: [Ruleset ex]

  Proof context: list of rulesets, each of which provides a number of axioms and rules.

- proofInput :: Formula ex

  Given expression

- proofResult :: Formula ex

  Result expression

- proofChain :: [Step ex]

  Chain of inference rule applications progressing from input to result

data Step ex Source #

Step in proof chain

The display name for a proof step comes from the display name of its consequence formula.

Constructors

Step |

Fields

- stepRule :: Rule ex

  Inference rule used

- stepAnt :: [Formula ex]

  Antecedents of inference rule

- stepCon :: Formula ex

  Named consequence of inference rule

#### Instances

Instances details

Show ex => Show (Step ex) Source # |
Instance details Defined in Swish.Proof Methods showsPrec :: Int -> Step ex -> ShowS Source # show :: Step ex -> String Source # showList :: [Step ex] -> ShowS Source #

checkProof :: (Expression ex, Ord ex) => Proof ex -> Bool Source #

Check consistency of given proof. The supplied rules and axioms are assumed to be correct.

explainProof :: (Expression ex, Ord ex) => Proof ex -> Maybe String Source #

Check proof. If there is an error then return information about the failing step.

checkStep Source #

Arguments

:: Ord ex |
=> [Rule ex] | rules
-> [ex] | antecedants
-> Step ex | the step to validate
-> Bool | `True` if the step is valid

A proof step is valid if rule is in list of rules and the antecedents are sufficient to obtain the conclusion and the antecedents are in the list of formulae already proven.

Note: this function depends on the ruleName of any rule being unique among all rules. In particular the name of the step rule being in correspondence with the name of one of the indicated valid rules of inference.

showProof Source #

Arguments

:: ShowLines ex |
=> String | newline string
-> Proof ex |
-> String |

Returns a simple string representation of a proof.

showsProof Source #

Arguments

:: ShowLines ex |
=> String | newline string
-> Proof ex |
-> ShowS |

Create a displayable form of a proof, returned as a `ShowS` value.

This function is intended to allow the calling function some control of multiline displays by providing:

1. the first line of the proof is not preceded by any text, so it may be appended to some preceding text on the same line,
2. the supplied newline string is used to separate lines of the formatted text, and may include any desired indentation, and
3. no newline is output following the final line of text.

showsFormula Source #

Arguments

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

Create a displayable form of a labelled formula