Data.Logic.Harrison.Herbrand

Documentation

pholds :: (PropositionalFormula formula atom, Ord atom) => Map atom Bool -> formula -> Bool

herbfuns :: forall pf atom term v f. (PropositionalFormula pf atom, Formula pf atom, Atom atom term v, Term term v f, IsString f, Ord f) => (atom -> Set (f, Int)) -> pf -> (Set (f, Int), Set (f, Int))

groundterms :: forall term v f. Term term v f => Set term -> Set (f, Int) -> Int -> Set term

groundtuples :: forall term v f. Term term v f => Set term -> Set (f, Int) -> Int -> Int -> Set [term]

herbloop :: forall lit atom v term f. (Literal lit atom, Term term v f, Atom atom term v) => (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)) -> (Set (Set lit) -> Failing Bool) -> Set (Set lit) -> Set term -> Set (f, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Failing (Set [term])

subst' :: forall lit atom term v f. (Literal lit atom, Atom atom term v, Term term v f) => Map v term -> lit -> lit

gilmore_loop :: (Literal lit atom, Term term v f, Atom atom term v, Ord lit) => Set (Set lit) -> Set term -> Set (f, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Failing (Set [term])

gilmore :: forall fof pf atom term v f. (FirstOrderFormula fof atom v, PropositionalFormula pf atom, Literal pf atom, Term term v f, Atom atom term v, IsString f, Ord pf) => pf -> (atom -> Set (f, Int)) -> fof -> Failing Int

dp_mfn :: (Ord b, Ord a) => Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)

dp_loop :: forall lit atom v term f. (Literal lit atom, Term term v f, Atom atom term v, Ord lit) => Set (Set lit) -> Set term -> Set (f, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Failing (Set [term])

davisputnam :: forall fof atom term v lit f. (FirstOrderFormula fof atom v, PropositionalFormula lit atom, Literal lit atom, Term term v f, Atom atom term v, IsString f, Ord lit) => lit -> (atom -> Set (f, Int)) -> fof -> Failing Int

dp_refine :: (Literal lit atom, Atom atom term v, Term term v f) => Set (Set lit) -> [v] -> Set [term] -> Set [term] -> Failing (Set [term])

dp_refine_loop :: forall lit atom term v f. (Literal lit atom, Term term v f, Atom atom term v) => Set (Set lit) -> Set term -> Set (f, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Failing (Set [term])

davisputnam' :: forall fof atom term lit v f pf. (FirstOrderFormula fof atom v, Literal lit atom, PropositionalFormula pf atom, Term term v f, Atom atom term v, IsString f) => lit -> pf -> (atom -> Set (f, Int)) -> fof -> Failing Int