bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermodule OWL2.Theorem where

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

81d182b21020b815887e9057959228546cf61b6bChristian Maederimport OWL2.AS

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport OWL2.MS

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederimport Data.List

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder-- | Adding annotations for theorems

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederaddImplied :: Axiom -> Axiom

fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederaddImplied a = case remImplied a of

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder PlainAxiom eith fb -> case eith of

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder Misc ans -> PlainAxiom (Misc (impliedTh: ans)) fb

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder _ -> case fb of

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder ListFrameBit mr lfb -> PlainAxiom eith

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder $ ListFrameBit mr (addImplListFB lfb)

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder AnnFrameBit ans afb -> PlainAxiom eith

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder $ AnnFrameBit (impliedTh : ans) afb

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian MaederaddImplListFB :: ListFrameBit -> ListFrameBit

ad270004874ce1d0697fb30d7309f180553bb315Christian MaederaddImplListFB lfb = case lfb of

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder AnnotationBit a -> AnnotationBit $ addImpliedAnnList a

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder ExpressionBit a -> ExpressionBit $ addImpliedAnnList a

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder ObjectBit a -> ObjectBit $ addImpliedAnnList a

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder DataBit a -> DataBit $ addImpliedAnnList a

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder IndividualSameOrDifferent a -> IndividualSameOrDifferent

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder $ addImpliedAnnList a

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ObjectCharacteristics a -> ObjectCharacteristics

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder $ addImpliedAnnList a

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder DataPropRange a -> DataPropRange $ addImpliedAnnList a

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder IndividualFacts a -> IndividualFacts $ addImpliedAnnList a

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaederaddImpliedAnnList :: AnnotatedList a -> AnnotatedList a

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaederaddImpliedAnnList [] = []

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederaddImpliedAnnList ((ans, b) : t) = (impliedTh : ans, b) : t

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederremImplied :: Axiom -> Axiom

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiremImplied (PlainAxiom eith fb) = case eith of

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder Misc ans -> PlainAxiom (Misc (remImpliedList ans)) fb

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder _ -> PlainAxiom eith

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder (

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder case fb of

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski ListFrameBit mr lfb -> ListFrameBit mr (remImplListFB lfb)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder AnnFrameBit ans afb -> AnnFrameBit (remImpliedList ans) afb

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder )

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederremImplListFB :: ListFrameBit -> ListFrameBit

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederremImplListFB lfb = case lfb of

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder AnnotationBit a -> AnnotationBit $ remImpliedAnnList a

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder ExpressionBit a -> ExpressionBit $ remImpliedAnnList a

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder ObjectBit a -> ObjectBit $ remImpliedAnnList a

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder DataBit a -> DataBit $ remImpliedAnnList a

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder IndividualSameOrDifferent a -> IndividualSameOrDifferent

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder $ remImpliedAnnList a

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder ObjectCharacteristics a -> ObjectCharacteristics

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder $ remImpliedAnnList a

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski DataPropRange a -> DataPropRange $ remImpliedAnnList a

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder IndividualFacts a -> IndividualFacts $ remImpliedAnnList a

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederremImplied1 :: (Annotations, a) -> (Annotations, a)

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederremImplied1 (ans, b) = (remImpliedList ans, b)

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian MaederremImpliedList :: Annotations -> Annotations

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederremImpliedList = filter (not . isToProve1)

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederremImpliedAnnList :: AnnotatedList a -> AnnotatedList a

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederremImpliedAnnList = map remImplied1

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederimpliedTh :: Annotation

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederimpliedTh = Annotation [] (mkQName "Implied")

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder (AnnValLit (Literal "true" (Typed (QN "" "string" False ""))))

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederisToProve1 :: Annotation -> Bool

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederisToProve1 anno = case anno of

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder Annotation _ aIRI (AnnValLit (Literal value (Typed _))) ->

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder localPart aIRI == "Implied" && isInfixOf "true" value

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder _ -> False

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

3c62e6ef442caf092adcbecf6fccd957dcd72689Christian MaederisToProveList :: (Annotations, a) -> Bool

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederisToProveList (ans, _) = any isToProve1 ans

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederisToProveAnnList :: AnnotatedList a -> Bool

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederisToProveAnnList = any isToProveList

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederisToProve :: Axiom -> Bool

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederisToProve (PlainAxiom eith fb) = case eith of

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Misc ans -> any isToProve1 ans

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder _ -> case fb of

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder ListFrameBit _ lfb -> isToProveLB lfb

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder AnnFrameBit ans _ -> any isToProve1 ans

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederisToProveLB :: ListFrameBit -> Bool

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian MaederisToProveLB fb = case fb of

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder AnnotationBit a -> isToProveAnnList a

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ExpressionBit a -> isToProveAnnList a

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder ObjectBit a -> isToProveAnnList a

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder DataBit a -> isToProveAnnList a

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder IndividualSameOrDifferent a -> isToProveAnnList a

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ObjectCharacteristics a -> isToProveAnnList a

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder DataPropRange a -> isToProveAnnList a

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder IndividualFacts a -> isToProveAnnList a

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder