Library for representation of unification on first-order terms.
This library implements a unification algorithm using reference tables.
Author: Michael Hanus, Jan-Hendrik Matthes, Jonas Oberschweiber, Bjoern Peemoeller
Version: August 2016
unify
:: [(Term a,Term a)] -> Either (UnificationError a) (FM Int (Term a))
Unifies a list of term equations. |
unifiable
:: [(Term a,Term a)] -> Bool
Checks whether a list of term equations can be unified. |