Logic_OWL11.hs revision a14767aeac3e78ed100f5b75e210ba563ee10dba
{-# OPTIONS -cpp #-}
{- |
Module : $Header$
Description : instance of the class Logic for OWL
Copyright : (c) Klaus Luettich, Heng Jiang, Uni Bremen 2002-2004
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : provisional
Portability : portable
Here is the place where the class Logic is instantiated for OWL DL.
__SROIQ__
-}
module OWL.Logic_OWL11 where
import Common.AS_Annotation
import Common.DefaultMorphism
import Common.Doc
import Common.DocUtils
import Common.ProofTree
import ATC.ProofTree ()
import Logic.Logic
import OWL.AS
import OWL.Print ()
import OWL.ATC_OWL ()
import OWL.Sign
import OWL.StaticAnalysis
#ifdef UNI_PACKAGE
import OWL.ProvePellet
#endif
data OWL11 = OWL11 deriving Show
instance Language OWL11 where
description _ =
"OWL DL -- Web Ontology Language Description Logic http://wwww.w3c.org/"
type OWL11_Morphism = DefaultMorphism Sign
instance Syntax OWL11 OntologyFile () ()
-- default implementation is fine!
-- OWL DL logic
instance Sentences OWL11 Sentence Sign OWL11_Morphism () where
map_sen OWL11 _ s = return s
print_named OWL11 namedSen =
pretty (sentence namedSen) <>
if null (senAttr namedSen) then empty
else space <> text "%%" <> text (senAttr namedSen)
<+> (case simpAnno namedSen of
Just True -> text "%%implied"
_ -> empty)
instance StaticAnalysis OWL11 OntologyFile Sentence
() ()
Sign
OWL11_Morphism
() () where
{- these functions are be implemented in OWL.StaticAna and OWL.Sign: -}
basic_analysis OWL11 = Just basicOWL11Analysis
empty_signature OWL11 = emptySign
signature_union OWL11 s = return . addSign s
final_union OWL11 = signature_union OWL11
inclusion OWL11 = defaultInclusion isSubSign
{- this function will be implemented in OWL.Taxonomy
theory_to_taxonomy OWL = convTaxo
-}
instance Logic OWL11 () OntologyFile Sentence () ()
Sign
OWL11_Morphism () () ProofTree where
-- stability _ = Testing
-- default implementations are fine
-- the prover uses HTk and IO functions from uni
#ifdef UNI_PACKAGE
provers OWL11 = [pelletProver]
cons_checkers OWL11 = [pelletConsChecker]
#endif