Safe Haskell | None |
---|

- 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

:: (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 -> BoolSource