编辑代码

type NormalisedExpr = Expr
type Reasoner = TBox -> ABox -> Bool
type Entailment = (Concept, Concept)

type Concept = String
type Role = String
type Desc = Either Concept Role

data Expr = Sub Concept Desc
          | SubConj Expr Expr
          | SubExists Role Desc
          deriving (Eq, Show)

normalise :: Expr -> NormalisedExpr
normalise (Sub c (Left d)) = Sub c (Left d)
normalise (Sub c (Right r)) = SubExists r (Left c)
normalise (SubConj e1 e2) = SubConj (normalise e1) (normalise e2)
normalise (SubExists r (Left c)) = SubExists r (Left c)
normalise (SubExists r (Right s)) = SubExists r (Right s)

satisfies :: TBox -> ABox -> Bool
satisfies tbox abox = all (\e -> any (\(c1, c2) -> check e c1 c2) abox) tbox
  where
    check (Sub c (Left d)) c1 c2 = c1 == c && c2 == d
    check (Sub c (Right r)) c1 c2 = any (\(c1', c2') -> c1' == c1 && c2' == c2 && (c2, c1) `elem` abox) abox
    check (SubConj e1 e2) c1 c2 = check e1 c1 c2 && check e2 c1 c2
    check (SubExists r (Left c)) c1 c2 = any (\(c', c'') -> c' == c1 && (r, c2) `elem` abox && c'' == c) abox
    check (SubExists r (Right s)) c1 c2 = any (\(c', c'') -> c' == c1 && (r, c') `elem` abox && (s, c2) `elem` abox && c'' == c) abox

entails :: TBox -> Entailment -> Bool
entails tbox (c1, c2) = satisfies tbox [(c1, c2)]

main :: IO ()
main = do
  let tbox = [Sub "A" (SubConj (Sub "B" (Right "r")) (SubExists "r" (Left "C"))),
              Sub "C" (SubExists "s" (Left "D")),
              SubConj (SubExists "r" (Left "T")) (Sub "B" (Left "D"))]
  let abox = [("T", "inst1"), ("B", "inst2"), ("C", "inst3"), ("D", "inst4")]
  putStrLn $ "TBox: " ++ show tbox
  putStrLn $ "ABox: " ++ show abox
  putStrLn $ "Entails A ⊑ D? " ++ show (entails tbox ("A", "D"))

TBox: [Sub "A" (SubConj (Sub "B" (Right "r")) (SubExists "r" (Left "C"))),Sub "C" (SubExists "s" (Left "D")),SubConj (SubExists "r" (Left "T")) (Sub "B" (Left "D"))]
ABox: [("T","inst1"),("B","inst2"),("C","inst3"),("D","inst4")]
Entails A ⊑ D? True