swish- A semantic web toolkit.

MaintainerDouglas Burke



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.



data Proof ex Source

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




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.




stepRule :: Rule ex

Inference rule used

stepAnt :: [Formula ex]

Antecedents of inference rule

stepCon :: Formula ex

Named consequence of inference rule


Show ex => Show (Step ex) 

checkProof :: Expression ex => Proof ex -> BoolSource

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

explainProof :: Expression ex => Proof ex -> Maybe StringSource

Check proof, and return identification of failing step.

checkStep :: Expression ex => [Rule ex] -> [ex] -> Step ex -> BoolSource

showProof :: ShowM ex => String -> Proof ex -> StringSource

Returns a simple string representation of a proof.

showsProof :: ShowM ex => String -> Proof ex -> ShowSSource

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 :: ShowM ex => String -> Formula ex -> ShowSSource

Create a displayable form of a labelled formula