| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Data.Logic.Resolution
- prove :: (Literal lit atom, Atom atom term v, Term term v f, Ord lit, Ord term, Ord v, AtomEq atom p term, Predicate p) => Maybe Int -> SetOfSupport lit v term -> SetOfSupport lit v term -> Set (ImplicativeForm lit) -> (Bool, SetOfSupport lit v term)
- getSetOfSupport :: (Literal lit atom, Atom atom term v, Term term v f, Ord lit, Ord term, Ord v) => Set (ImplicativeForm lit) -> Set (ImplicativeForm lit, Map v term)
- type SetOfSupport lit v term = Set (Unification lit v term)
- type Unification lit v term = (ImplicativeForm lit, Map v term)
- isRenameOfAtomEq :: (AtomEq atom p term, Term term v f) => atom -> atom -> Bool
- getSubstAtomEq :: forall atom p term v f. (AtomEq atom p term, Term term v f) => Map v term -> atom -> Map v term
Documentation
Arguments
| :: (Literal lit atom, Atom atom term v, Term term v f, Ord lit, Ord term, Ord v, AtomEq atom p term, Predicate p) | |
| => Maybe Int | Recursion limit. We continue recursing until this becomes zero. If it is negative it may recurse until it overflows the stack. |
| -> SetOfSupport lit v term | |
| -> SetOfSupport lit v term | |
| -> Set (ImplicativeForm lit) | |
| -> (Bool, SetOfSupport lit v term) |
getSetOfSupport :: (Literal lit atom, Atom atom term v, Term term v f, Ord lit, Ord term, Ord v) => Set (ImplicativeForm lit) -> Set (ImplicativeForm lit, Map v term) Source
Convert the "question" to a set of support.
type SetOfSupport lit v term = Set (Unification lit v term) Source
type Unification lit v term = (ImplicativeForm lit, Map v term) Source
isRenameOfAtomEq :: (AtomEq atom p term, Term term v f) => atom -> atom -> Bool Source