Data.Logic.Harrison.Tableaux

Documentation

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

unifyAtomsEq :: forall v f atom p term. (AtomEq atom p term, Term term v f) => Map v term -> atom -> atom -> Failing (Map v term)

deepen :: (Int -> Failing t) -> Int -> Maybe Int -> Failing (t, Int)

Try f with higher and higher values of n until it succeeds, or optional maximum depth limit is exceeded.