Logic_OWL2.hs revision cdcf5d3f1e79d8798d77efa29e6193af94ea0604
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances #-}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{-# OPTIONS -w #-}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- |
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : ./OWL2/Logic_OWL2.hs
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannDescription : instance of the class Logic for OWL2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Christian Maeder, DFKI GmbH 2011
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : GPLv2 or higher, see LICENSE.txt
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : Christian.Maeder@dfki.de
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : provisional
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : non-portable
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannHere is the place where the class Logic is instantiated for OWL2.
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule OWL2.Logic_OWL2 where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport ATC.ProofTree ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.AS_Annotation
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Consistency
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.DefaultMorphism
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Doc
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.DocUtils
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.ProofTree
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.ProverTools
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.Char (isAlpha)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.Monoid
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Data.Map as Map
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Data.Set as Set
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Logic.Logic
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.AS
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.ATC_OWL2 ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.ColimSign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Conservativity
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.MS
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.MS2Ship
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.ManchesterParser
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.ManchesterPrint
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Morphism
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Parse
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Print ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.ProfilesAndSublogics
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.ProveFact
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.ProvePellet
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Rename
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.StaticAnalysis
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Symbols
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Taxonomy
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.Theorem
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OWL2.ExtractModule
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanndata OWL2 = OWL2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Show OWL2 where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann show _ = "OWL"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Language OWL2 where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann description _ =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann "OWL -- Web Ontology Language http://www.w3.org/TR/owl2-overview/"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Category Sign OWLMorphism where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ide sig = inclOWLMorphism sig sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann dom = osource
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann cod = otarget
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann legal_mor = legalMor
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann isInclusion = isOWLInclusion
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann composeMorphisms = composeMor
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Monoid Ontology where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann mempty = emptyOntology []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann mappend (Ontology n i1 a1 f1) (Ontology _ i2 a2 f2) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Ontology n (i1 ++ i2) (a1 ++ a2) $ f1 ++ f2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Monoid OntologyDocument where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann mempty = emptyOntologyDoc
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann mappend (OntologyDocument p1 o1) (OntologyDocument p2 o2) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann OntologyDocument (Map.union p1 p2) $ mappend o1 o2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Syntax OWL2 OntologyDocument Entity SymbItems SymbMapItems where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann parsersAndPrinters OWL2 = addSyntax "Ship" (basicSpec, ppShipOnt)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ addSyntax "Manchester" (basicSpec, pretty)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ makeDefault (basicSpec, pretty)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann parseSingleSymbItem OWL2 = Just symbItem
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann parse_symb_items OWL2 = Just symbItems
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann parse_symb_map_items OWL2 = Just symbMapItems
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann symb_items_name OWL2 = symbItemsName
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Sentences OWL2 Axiom Sign OWLMorphism Entity where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_sen OWL2 = mapSen
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann print_named OWL2 = printOneNamed
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sym_of OWL2 = singletonList . symOf
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann symmap_of OWL2 = symMapOf
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sym_name OWL2 = entityToId
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sym_label OWL2 = label
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann fullSymName OWL2 s = let
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann i = cutIRI s
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann x = expandedIRI i
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in if null x then getPredefName i else x
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann symKind OWL2 = takeWhile isAlpha . showEntityType . entityKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann symsOfSen OWL2 _ = Set.toList . symsOfAxiom
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann pair_symbols OWL2 = pairSymbols
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance StaticAnalysis OWL2 OntologyDocument Axiom
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann SymbItems SymbMapItems
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann OWLMorphism
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Entity RawSymb where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basic_analysis OWL2 = Just basicOWL2Analysis
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann stat_symb_items OWL2 s = return . statSymbItems s
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann stat_symb_map_items OWL2 = statSymbMapItems
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann convertTheory OWL2 = Just convertBasicTheory
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann empty_signature OWL2 = emptySign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann signature_union OWL2 = uniteSign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann intersection OWL2 = intersectSign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann signatureDiff OWL2 s = return . diffSig s
final_union OWL2 = signature_union OWL2
is_subsig OWL2 = isSubSign
subsig_inclusion OWL2 s = return . inclOWLMorphism s
matches OWL2 = matchesSym
symbol_to_raw OWL2 = ASymbol
add_symb_to_sign OWL2 = addSymbToSign
induced_from_morphism OWL2 = inducedFromMor
cogenerated_sign OWL2 = cogeneratedSign
generated_sign OWL2 = generatedSign
signature_colimit OWL2 = return . signColimit
corresp2th OWL2 = corr2theo
equiv2cospan OWL2 = addEquiv
extract_module OWL2 = extractModule
#ifdef UNI_PACKAGE
theory_to_taxonomy OWL2 = onto2Tax
#endif
instance Logic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems
Sign
OWLMorphism Entity RawSymb ProofTree where
empty_proof_tree OWL2 = emptyProofTree
-- just a selection of sublogics
all_sublogics OWL2 = bottomS : concat allProfSubs ++ [topS]
bottomSublogic OWL2 = Just bottomS
sublogicDimensions OWL2 = allProfSubs
parseSublogic OWL2 _ = Just topS -- ignore sublogics
provers OWL2 = [pelletProver, pelletEL, factProver]
cons_checkers OWL2 = [pelletConsChecker, factConsChecker]
conservativityCheck OWL2 = map
(\ ct -> ConservativityChecker ("Locality_" ++ ct)
(checkOWLjar localityJar) $ conserCheck ct)
["BOTTOM_BOTTOM", "TOP_BOTTOM", "TOP_TOP"]
stability OWL2 = Stable
instance SemiLatticeWithTop ProfSub where
lub = maxS
top = topS
instance SublogicName ProfSub where
sublogicName = nameS
instance MinSublogic ProfSub Axiom where
minSublogic = psAxiom
instance MinSublogic ProfSub OWLMorphism where
minSublogic = sMorph
instance ProjectSublogic ProfSub OWLMorphism where
projectSublogic = prMorph
instance MinSublogic ProfSub Sign where
minSublogic = sSig
instance ProjectSublogic ProfSub Sign where
projectSublogic = prSign
instance MinSublogic ProfSub SymbItems where
minSublogic = const topS
instance MinSublogic ProfSub SymbMapItems where
minSublogic = const topS
instance MinSublogic ProfSub Entity where
minSublogic = const topS
instance MinSublogic ProfSub OntologyDocument where
minSublogic = profilesAndSublogic
instance ProjectSublogicM ProfSub SymbItems where
projectSublogicM = const Just
instance ProjectSublogicM ProfSub SymbMapItems where
projectSublogicM = const Just
instance ProjectSublogicM ProfSub Entity where
projectSublogicM = const Just
instance ProjectSublogic ProfSub OntologyDocument where
projectSublogic = prOntDoc