HyLo.Model

Documentation

data Model w n p r

Instances

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r, w) (Formula n p r) n p r

Defined in HyLo.Model

Methods

(|=) :: (Model w n p r, w) -> Formula n p r -> Bool

(Read w, Read n, Read p, Read r, Ord w, Ord n, Ord p, Ord r) => Read (Model w n p r)

Defined in HyLo.Model

Methods

readsPrec :: Int -> ReadS (Model w n p r)

readList :: ReadS [Model w n p r]

readPrec :: ReadPrec (Model w n p r)

readListPrec :: ReadPrec [Model w n p r]

(Show w, Show n, Show p, Show r) => Show (Model w n p r)

Defined in HyLo.Model

Methods

showsPrec :: Int -> Model w n p r -> ShowS

show :: Model w n p r -> String

showList :: [Model w n p r] -> ShowS

HasSignature (Model w n p r)

Defined in HyLo.Model

Associated Types

type NomsOf (Model w n p r) :: Type

type PropsOf (Model w n p r) :: Type

type RelsOf (Model w n p r) :: Type

Methods

getSignature :: Model w n p r -> Signature (NomsOf (Model w n p r)) (PropsOf (Model w n p r)) (RelsOf (Model w n p r))

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r) (Formula n p r) n p r

Defined in HyLo.Model

Methods

(|=) :: Model w n p r -> Formula n p r -> Bool

type NomsOf (Model w n p r)

Defined in HyLo.Model

type NomsOf (Model w n p r) = n

type PropsOf (Model w n p r)

Defined in HyLo.Model

type PropsOf (Model w n p r) = p

type RelsOf (Model w n p r)

Defined in HyLo.Model

type RelsOf (Model w n p r) = r

worlds :: Model w n p r -> Set w

succs :: Model w n p r -> r -> w -> Set w

valP :: Model w n p r -> p -> Set w

valN :: Model w n p r -> n -> w

model :: (RelRepr rs r w, ValRepr ps p w, ValNomRepr ns n w) => Set w -> rs -> ps -> ns -> Signature n p r -> Model w n p r

equiv :: (Eq w, Eq n, Eq p, Eq r) => Model w n p r -> Model w n p r -> Bool

expand :: (Ord n, Ord p, Ord r) => Signature n p r -> Model w n p r -> Model w n p r

setSignature :: (Ord n, Ord p, Ord r) => Signature n p r -> Model w n p r -> Model w n p r

(??) :: Eq n => Model w n p r -> (n, w) -> Model w n p r

removeWorld :: Ord w => w -> Model w n p r -> Model w n p r

removeWorlds :: Ord w => Set w -> Model w n p r -> Model w n p r

countInModel :: (Ord w, Ord n, Ord p, Ord r) => Formula n p r -> Model w n p r -> Int

namesOf :: Eq w => w -> Model w n p r -> [n]

propsOf :: Ord w => w -> Model w n p r -> [p]

class ModelsRel m f n p r | m -> n, m -> p, m -> r, f -> n, f -> p, f -> r where

Methods

(|=) :: m -> f -> Bool infix 9

Instances

(Ord r, Ord n, Ord p, ModelsRel (Model n n p r, n) f n p r) => ModelsRel (HerbrandModel n p r, n) f n p r

Defined in HyLo.Model.Herbrand

Methods

(|=) :: (HerbrandModel n p r, n) -> f -> Bool

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r, w) (Formula n p r) n p r

Defined in HyLo.Model

Methods

(|=) :: (Model w n p r, w) -> Formula n p r -> Bool

(Ord r, Ord n, Ord p, ModelsRel (Model n n p r) f n p r) => ModelsRel (HerbrandModel n p r) f n p r

Defined in HyLo.Model.Herbrand

Methods

(|=) :: HerbrandModel n p r -> f -> Bool

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r) (Formula n p r) n p r

Defined in HyLo.Model

Methods

(|=) :: Model w n p r -> Formula n p r -> Bool

(|/=) :: ModelsRel m f n p r => m -> f -> Bool infix 9