Portability  H98 

Stability  experimental 
Maintainer  Douglas 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 prooffinding strategy.
 data Proof ex = Proof {
 proofContext :: [Ruleset ex]
 proofInput :: Formula ex
 proofResult :: Formula ex
 proofChain :: [Step ex]
 data Step ex = Step {}
 checkProof :: Expression ex => Proof ex > Bool
 explainProof :: Expression ex => Proof ex > Maybe String
 checkStep :: Expression ex => [Rule ex] > [ex] > Step ex > Bool
 showProof :: ShowM ex => String > Proof ex > String
 showsProof :: ShowM ex => String > Proof ex > ShowS
 showsFormula :: ShowM ex => String > Formula ex > ShowS
Documentation
Proof is a structure that presents a chain of rule applications that yield a result expression from a given expression
Proof  

Step in proof chain
The display name for a proof step comes from the display name of its consequence formula.
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. If there is an error then return information about the failing step.
:: Expression ex  
=> [Rule ex]  rules 
> [ex]  a ntecedants 
> Step ex  the step to validate 
> Bool 

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.
Returns a simple string representation of a proof.
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:
 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,
 the supplied newline string is used to separate lines of the formatted text, and may include any desired indentation, and
 no newline is output following the final line of text.