ProverState.hs revision a604cbad8e2202147b5c6bb9f2e06ae61162d654
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : Interface to the OWL Ontology provers.
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Heng Jiang, Uni Bremen 2004-2008
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederMaintainer : Christian.Maeder@dfki.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederprover states for pellet and fact++
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowskidata ProverState = ProverState
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder { ontologySign :: Sign
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , initialState :: [Named Axiom]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder } deriving Show
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederowlProverState :: Sign
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> [Named Axiom]
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder -> ProverState
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederowlProverState sig oSens _ = ProverState
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder { ontologySign = sig
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder , initialState = filter isAxiom oSens }
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Inserts a named OWL axiom into the prover state.
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichinsertOWLAxiom :: ProverState -- ^ prover state containing initial logical part
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder -> Named Axiom -- ^ goal to add
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder -> ProverState
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian MaederinsertOWLAxiom pps s = pps { initialState = initialState pps ++ [s] }
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian MaedershowOWLProblemS :: ProverState
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder -> String -- ^ formatted output
57a2436f9d44e37042498a3b3dfacd301d91bb6dChristian MaedershowOWLProblemS pst =
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder let namedSens = initialState pst
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder sign = ontologySign pst
d4892fa7401ceef014ea59d2d900773eaf88fcbdChristian Maeder in show $ printOWLBasicTheory (sign, filter isAxiom namedSens)
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder Pretty printing OWL goal for pellet or fact++
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichshowOWLProblem :: ProverState -- ^ prover state containing initial logical part
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> Named Axiom -- ^ goal to print
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> IO String -- ^ formatted output of the goal
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian MaedershowOWLProblem pst nGoal =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let sign = ontologySign pst
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder in return $ showOWLProblemS pst
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ++ "\n\nEntailments:\n\n" ++ show (printOWLBasicTheory (sign, [nGoal]))