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

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

(Show n, Show p, Show r) => Show (HerbrandModel n p r)

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

(Ord r, Ord n, Ord p) => HasSignature (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

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

unit_tests :: UnitTest