HyLo.Model.Herbrand

Documentation

data HerbrandModel n p r

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

Methods

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

(Ord r, Ord n, Ord p) => HasSignature (HerbrandModel n p r)

Associated Types

type NomsOf (HerbrandModel n p r) :: *

type PropsOf (HerbrandModel n p r) :: *

type RelsOf (HerbrandModel n p r) :: *

Methods

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

(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

Methods

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

type NomsOf (HerbrandModel n p r)

type NomsOf (HerbrandModel n p r) = n

type PropsOf (HerbrandModel n p r)

type PropsOf (HerbrandModel n p r) = p

type RelsOf (HerbrandModel n p r)

type RelsOf (HerbrandModel n p r) = r

herbrand :: (Ord n, Ord p, Ord r) => Set (n, n) -> Set (n, p) -> Set (n, r, n) -> HerbrandModel n p r

inducedModel :: (Ord r, Ord n, Ord p) => HerbrandModel n p r -> Model n n p r

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

removeWorld :: (Ord n, Ord p, Ord r) => n -> HerbrandModel n p r -> HerbrandModel n p r