Safe Haskell | None |
---|---|
Language | Haskell98 |
Documentation
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)) Source
groundtuples :: forall term v f. Term term v f => Set term -> Set (f, Int) -> Int -> Int -> Set [term] Source
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]) Source
subst' :: forall lit atom term v f. (Literal lit atom, Atom atom term v, Term term v f) => Map v term -> lit -> lit Source
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]) Source
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 Source
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]) Source
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 Source
dp_refine :: (Literal lit atom, Atom atom term v, Term term v f) => Set (Set lit) -> [v] -> Set [term] -> Set [term] -> Failing (Set [term]) Source
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]) Source
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 Source