Module Rewriting.Unification

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: February 2020

Summary of exported operations:

unify :: Eq a => [(Term a,Term a)] -> Either (UnificationError a) (Map Int (Term a))  Deterministic 
Unifies a list of term equations.
unifiable :: Eq a => [(Term a,Term a)] -> Bool  Deterministic 
Checks whether a list of term equations can be unified.

Exported operations:

unify :: Eq a => [(Term a,Term a)] -> Either (UnificationError a) (Map Int (Term a))  Deterministic 

Unifies a list of term equations. Returns either a unification error or a substitution.

unifiable :: Eq a => [(Term a,Term a)] -> Bool  Deterministic 

Checks whether a list of term equations can be unified.