7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk{- |

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkModule : ./OWL2/ProverState.hs

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkDescription : Interface to the OWL Ontology provers.

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkCopyright : (c) Heng Jiang, Uni Bremen 2004-2008

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkLicense : GPLv2 or higher, see LICENSE.txt

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkMaintainer : Christian.Maeder@dfki.de

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkStability : provisional

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkPortability : portable

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkprover states for pellet and fact++

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk-}

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkmodule OWL2.ProverState where

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkimport Logic.Prover

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkimport OWL2.MS

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkimport OWL2.Morphism

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkimport OWL2.Sign

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkimport OWL2.ManchesterPrint

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkimport OWL2.XMLConversion

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkimport Common.AS_Annotation

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkdata ProverState = ProverState

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk { ontologySign :: Sign,

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk initialState :: [Named Axiom]

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk } deriving Show

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkowlProverState :: Sign -> [Named Axiom]

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk -> ProverState

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkowlProverState sig oSens _ = ProverState

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk { ontologySign = sig,

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk initialState = filter isAxiom oSens }

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk{- |

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk Inserts a named OWL2 axiom into the prover state.

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk-}

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkinsertOWLAxiom :: ProverState -- ^ prover state containing initial logical part

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk -> Named Axiom -- ^ goal to add

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk -> ProverState

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkinsertOWLAxiom pps s = pps { initialState = initialState pps ++ [s] }

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkshowOWLProblemS :: ProverState -> String -- ^ formatted output

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkshowOWLProblemS pst =

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk let namedSens = initialState pst

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk sign = ontologySign pst

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk in mkODoc sign (filter isAxiom namedSens)

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk{- |

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk Pretty printing OWL goal for pellet or fact++

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk-}

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkshowOWLProblem :: ProverState -- ^ prover state containing initial logical part

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk -> Named Axiom -- ^ goal to print

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk -> IO String -- ^ formatted output of the goal

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkshowOWLProblem pst nGoal =

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk let sign = ontologySign pst

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk in return $ showOWLProblemS pst

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk ++ "\n\nEntailments:\n\n" ++ show (printOWLBasicTheory (sign, [nGoal]))

7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk