Safe Haskell | None |
---|

# 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 -> litSource

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) => (atom -> Set (f, Int)) -> fof -> Failing IntSource

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) => (atom -> Set (f, Int)) -> fof -> Failing IntSource

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) => (atom -> Set (f, Int)) -> fof -> Failing IntSource