swish-0.2.1: Swish/HaskellRDF/Proof.hs
--------------------------------------------------------------------------------
-- $Id: Proof.hs,v 1.19 2004/01/07 19:49:12 graham Exp $
--
-- Copyright (c) 2003, G. KLYNE. All rights reserved.
-- See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
-- Module : Proof
-- Copyright : (c) 2003, Graham Klyne
-- License : GPL V2
--
-- Maintainer : Graham Klyne
-- Stability : provisional
-- Portability : H98
--
-- 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.
--
--------------------------------------------------------------------------------
module Swish.HaskellRDF.Proof
( Proof(..), Step(..)
, checkProof, explainProof, checkStep, showProof, showsProof, showsFormula )
where
import Swish.HaskellRDF.Ruleset
( Ruleset(..)
, makeRuleset, getRulesetNamespace, getRulesetAxioms, getRulesetRules )
import Swish.HaskellRDF.Rule
( Expression(..), Formula(..), Rule(..)
, fwdCheckInference
, showsFormula, showsFormulae, showsWidth )
import Swish.HaskellUtils.Namespace
( Namespace(..)
, ScopedName(..)
, getScopePrefix, getScopeURI
, getQName, getScopedNameURI )
import Swish.HaskellUtils.ShowM
( ShowM(..), showm )
import Swish.HaskellUtils.ListHelpers
( subset )
import Data.List
( union, intersect, intersperse )
import Data.Maybe
( isJust, fromJust, catMaybes )
------------------------------------------------------------
-- Proof framework
------------------------------------------------------------
-- |Step in proof chain
--
-- The display name for a proof step comes from the display name of its
-- consequence formula.
data Step ex = Step
{ stepRule :: Rule ex -- ^ Inference rule used
, stepAnt :: [Formula ex] -- ^ Antecedents of inference rule
, stepCon :: Formula ex -- ^ Named consequence of inference rule
} deriving Show
-- |Proof is a structure that presents a chain of rule applications
-- that yield a result expression from a given expression
data Proof ex = Proof
{ 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
}
-- |Return a list of axioms from all the rulesets in a proof
proofAxioms = concat . map rsAxioms . proofContext
-- |Return a list of rules from all the rulesets in a proof
proofRules = concat . map rsRules . proofContext
-- |Return list of axioms actually referenced by a proof
proofAxiomsUsed :: Proof ex -> [Formula ex]
proofAxiomsUsed proof = foldl union [] $ map stepAxioms (proofChain proof)
where
stepAxioms st = stepAnt st `intersect` proofAxioms proof
-- |Check consistency of given proof.
-- The supplied rules and axioms are assumed to be correct.
checkProof :: (Expression ex) => Proof ex -> Bool
checkProof pr =
checkProof1 (proofRules pr) initExpr (proofChain pr) goalExpr
where
initExpr = (formExpr $ proofInput pr):(map formExpr $ proofAxioms pr)
goalExpr = (formExpr $ proofResult pr)
checkProof1 :: (Expression ex) => [Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
checkProof1 _ prev [] res = res `elem` prev
checkProof1 rules prev (st:steps) res =
checkStep rules prev st &&
checkProof1 rules ((formExpr $ stepCon st):prev) steps res
-- 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.
checkStep :: (Expression ex) => [Rule ex] -> [ex] -> Step ex -> Bool
checkStep rules prev step =
-- Rule name is one of supplied rules, and
(ruleName srul `elem` map ruleName rules) &&
-- Antecedent expressions are all previously accepted expressions
(sant `subset` prev) &&
-- Inference rule yields concequence from antecendents
checkInference srul sant scon
where
-- Rule from proof step:
srul = stepRule step
-- Antecedent expressions from proof step:
sant = map formExpr $ stepAnt step
-- Consequentent expression from proof step:
scon = formExpr $ stepCon step
{-
(formExpr (stepCon step) `elem` sfwd)
-- (or $ map (`subset` sant) sbwd)
where
-- Rule from proof step:
srul = stepRule step
-- Antecedent expressions from proof step:
sant = map formExpr $ stepAnt step
-- Forward chaining from antecedents of proof step
scon = map formExpr $ stepCon step
-- Forward chaining from antecedents of proof step
sfwd = fwdApply srul sant
-- Backward chaining from consequent of proof step
-- (Does not work because of introduction of existentials)
sbwd = bwdApply srul (formExpr $ stepCon step)
-}
-- |Check proof, and return identification of failing step.
explainProof ::
(Expression ex) => Proof ex -> Maybe String
explainProof pr =
explainProof1 (proofRules pr) initExpr (proofChain pr) goalExpr
where
initExpr = (formExpr $ proofInput pr):(map formExpr $ proofAxioms pr)
goalExpr = (formExpr $ proofResult pr)
explainProof1 ::
(Expression ex) => [Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
explainProof1 _ prev [] res =
if res `elem` prev then Nothing else Just "Result not demonstrated"
explainProof1 rules prev (st:steps) res =
case explainStep rules prev st of
Nothing -> explainProof1 rules ((formExpr $ stepCon st):prev) steps res
Just ex -> Just ("Invalid step: "++show (formName $ stepCon st)++": "++ex)
-- 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.
--
-- Return Nothing if step is OK, or Just string describing failure
--
explainStep :: (Expression ex) => [Rule ex] -> [ex] -> Step ex -> Maybe String
explainStep rules prev step =
if null errors then Nothing else Just $ concat (intersperse ", " errors)
where
-- Rule from proof step:
srul = stepRule step
-- Antecedent expressions from proof step:
sant = map formExpr $ stepAnt step
-- Consequentent expression from proof step:
scon = formExpr $ stepCon step
-- Tests for step to be valid
errors = catMaybes
-- Rule name is one of supplied rules, and
[ require (ruleName srul `elem` map ruleName rules)
("rule "++show (ruleName srul)++" not present")
-- Antecedent expressions are all previously accepted expressions
, require (sant `subset` prev)
("antecedent not axiom or previous result")
-- Inference rule yields consequence from antecedents
, require (checkInference srul sant scon)
("rule does not deduce consequence from antecedents")
]
require b s = if b then Nothing else Just s
-- |showsProof
-- 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.
showsProof :: (ShowM ex) => String -> Proof ex -> ShowS
showsProof newline proof =
if null axioms then shProof else shAxioms . shProof
where
axioms = proofAxiomsUsed proof
shAxioms =
showString ("Axioms:" ++ newline) .
showsFormulae newline (proofAxiomsUsed proof) newline
shProof =
showString ("Input:" ++ newline) .
showsFormula newline (proofInput proof) .
showString (newline ++ "Proof:" ++ newline) .
showsSteps newline (proofChain proof)
-- |showProof
-- Returns a simple string representation of a proof.
showProof :: (ShowM ex) => String -> Proof ex -> String
showProof newline proof = showsProof newline proof ""
-- |showsSteps
-- Create a displayable form of a list of labelled proof steps
showsSteps :: (ShowM ex) => String -> [Step ex] -> ShowS
showsSteps _ [] = id
showsSteps newline [s] = showsStep newline s
showsSteps newline (s:ss) = showsStep newline s .
showString newline .
showsSteps newline ss
-- |showsStep
-- Create a displayable form of a labelled proof step.
showsStep :: (ShowM ex) => String -> Step ex -> ShowS
showsStep newline s = showsFormula newline (stepCon s) .
showString newline .
showString (" (by ["++rulename++"] from "++antnames++")")
where
rulename = show . ruleName $ stepRule s
antnames = showNames $ map (show . formName) (stepAnt s)
-- |showNames
-- Return a string containing a list of names.
showNames :: [String] -> String
showNames [] = "<nothing>"
showNames [n] = showName n
showNames [n1,n2] = showName n1 ++ " and " ++ showName n2
showNames (n1:ns) = showName n1 ++ ", " ++ showNames ns
-- |showNames
-- Return a string representing a single name.
showName n = "["++n++"]"
--------------------------------------------------------------------------------
--
-- Copyright (c) 2003, G. KLYNE. All rights reserved.
--
-- This file is part of Swish.
--
-- Swish is free software; you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation; either version 2 of the License, or
-- (at your option) any later version.
--
-- Swish is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-- GNU General Public License for more details.
--
-- You should have received a copy of the GNU General Public License
-- along with Swish; if not, write to:
-- The Free Software Foundation, Inc.,
-- 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
--
--------------------------------------------------------------------------------
-- $Source: /file/cvsdev/HaskellRDF/Proof.hs,v $
-- $Author: graham $
-- $Revision: 1.19 $
-- $Log: Proof.hs,v $
-- Revision 1.19 2004/01/07 19:49:12 graham
-- Reorganized RDFLabel details to eliminate separate language field,
-- and to use ScopedName rather than QName.
-- Removed some duplicated functions from module Namespace.
--
-- Revision 1.18 2003/12/18 18:27:47 graham
-- Datatyped literal inferences all working
-- (except equivalent literals with different datatypes)
--
-- Revision 1.17 2003/12/11 19:11:07 graham
-- Script processor passes all initial tests.
--
-- Revision 1.16 2003/09/30 20:02:39 graham
-- Proof mechanisms now use scoped names and rulesets.
-- Move some functionality between modules so that RDFProofCheck
-- contains less generic code.
--
-- Revision 1.15 2003/09/30 16:39:41 graham
-- Refactor proof code to use new ruleset logic.
-- Moved some support code from RDFProofCheck to RDFRuleset.
--
-- Revision 1.14 2003/09/24 18:50:52 graham
-- Revised module format to be Haddock compatible.
--
-- Revision 1.13 2003/07/02 13:51:14 graham
-- Intermediate save: partially coded RDFS rules.
--
-- Revision 1.12 2003/07/01 14:20:30 graham
-- Added instance entailment to proof check module.
--
-- Revision 1.11 2003/06/27 20:46:00 graham
-- Coded initial version of RDF simple entailment rule.
-- New rule still needs testing, but other test cases still OK.
--
-- Revision 1.10 2003/06/26 15:37:23 graham
-- Added rdfQueryInstance, and tests, all works.
--
-- Revision 1.9 2003/06/25 21:16:53 graham
-- Reworked N3 formatting logic to support proof display.
-- Basic proof display is working.
--
-- Revision 1.8 2003/06/24 23:08:18 graham
-- Replaced Rule class with algebraic data type
--
-- Revision 1.7 2003/06/24 19:56:31 graham
-- Basic proof-check now works
--
-- Revision 1.6 2003/06/19 19:49:07 graham
-- RDFProofCheck compiles, but test fails
--
-- Revision 1.5 2003/06/18 18:40:08 graham
-- Basic proof backchaining tests OK.
-- Next: add filtering on variable bindings.
--
-- Revision 1.4 2003/06/13 21:40:08 graham
-- Graph closure forward chaining works.
-- Backward chaining generates existentials.
-- Some problems with query logic for backward chaining.
--
-- Revision 1.3 2003/06/10 01:04:46 graham
-- Proof framework in progress; compiles, incomplete
--
-- Revision 1.2 2003/06/04 00:49:53 graham
-- Proof module compiles OK
--
-- Revision 1.1 2003/06/03 19:24:54 graham
-- Started work on inference/proof module
--