1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel ManceDescription : Comorphism from Propostional Logic to OWL 2
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel ManceCopyright : (c) Felix Gabriel Mance
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel ManceLicense : GPLv2 or higher, see LICENSE.txt
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel ManceMaintainer : f.mance@jacobs-university.de
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel ManceStability : provisional
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancePortability : non-portable (via Logic.Logic)
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified OWL2.Morphism as OWLMor
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified OWL2.ProfilesAndSublogics as OWLSub
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified OWL2.Sign as OWLSign
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified OWL2.Logic_OWL2 as OWLLogic
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified OWL2.Symbols as OWLSym
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified Propositional.Logic_Propositional as PLogic
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport Propositional.AS_BASIC_Propositional
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified Propositional.Sublogic as PSL
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified Propositional.Sign as PSign
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified Propositional.Morphism as PMor
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified Propositional.Symbol as PSymbol
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceimport qualified Data.Set as Set
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mancedata Propositional2OWL2 = Propositional2OWL2 deriving Show
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceinstance Language Propositional2OWL2
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Manceinstance Comorphism Propositional2OWL2
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance SYMB_MAP_ITEMS
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance OntologyDocument
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance sourceLogic Propositional2OWL2 = PLogic.Propositional
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance sourceSublogic Propositional2OWL2 = PSL.top
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance targetLogic Propositional2OWL2 = OWLLogic.OWL2
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance mapSublogic Propositional2OWL2 = Just . mapSub -- TODO
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance map_theory Propositional2OWL2 = mapTheory
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance isInclusionComorphism Propositional2OWL2 = True
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance has_model_expansion Propositional2OWL2 = True
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemkOWLDeclaration :: ClassExpression -> Axiom
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemkOWLDeclaration ex = PlainAxiom (ClassEntity $ Expression $ setPrefix "owl"
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ mkIRI thingS) $ ListFrameBit (Just SubClass) $ ExpressionBit [([], ex)]
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskitokToIRI :: Token -> IRI
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskitokToIRI = idToIRI . simpleIdToId
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapFormula :: FORMULA -> ClassExpression
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapFormula f = case f of
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski False_atom _ -> Expression $ mkIRI nothingS
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski True_atom _ -> Expression $ mkIRI thingS
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski Predication p -> Expression $ tokToIRI p
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance Negation nf _ -> ObjectComplementOf $ mapFormula nf
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance Conjunction fl _ -> ObjectJunction IntersectionOf $ map mapFormula fl
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance Disjunction fl _ -> ObjectJunction UnionOf $ map mapFormula fl
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance Implication a b _ -> ObjectJunction UnionOf [ObjectComplementOf
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance $ mapFormula a, mapFormula b]
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance Equivalence a b _ -> ObjectJunction IntersectionOf $ map mapFormula
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance [Implication a b nullRange, Implication b a nullRange]
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapPredDecl :: PRED_ITEM -> [Axiom]
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapPredDecl (Pred_item il _) = map (mkOWLDeclaration . Expression
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski . tokToIRI) il
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapAxiomItems :: Annoted FORMULA -> Axiom
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapAxiomItems = mkOWLDeclaration . mapFormula . item
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapBasicItems :: BASIC_ITEMS -> [Axiom]
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapBasicItems bi = case bi of
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance Pred_decl p -> mapPredDecl p
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance Axiom_items al -> map mapAxiomItems al
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapBasicSpec :: BASIC_SPEC -> [Axiom]
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapBasicSpec (Basic_spec il) = concatMap (mapBasicItems . item) il
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapSign ps = OWLSign.emptySign {OWLSign.concepts = Set.fromList
c505f62dff03727dc14a1f08be48208540d78d4aChristian Maeder $ map idToIRI $ Set.toList $ PSign.items ps}
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel MancemapTheory :: (PSign.Sign, [Named FORMULA])
8b6fee95f9d848c78824b9aeccdf9a081efaebd3Felix Gabriel Mance -> Result (OWLSign.Sign, [Named Axiom])
11b2f40b44151371573b93dfefff7dc3f8ce883bChristian MaedermapTheory (psig, fl) = return (mapSign psig, map
11b2f40b44151371573b93dfefff7dc3f8ce883bChristian Maeder (mapNamed $ mkOWLDeclaration . mapFormula) fl)