README About Versions Source Modules

LogicUS.FOL.Unification

This module allows to calculate the Maximum General Unificator (MGU)

MGU

termMGU : Term -> Term -> Maybe Substitution

It calculates a Maximum General Unificator between two terms, if it exists.

termsMGU : List Term -> List Term -> Maybe Substitution

It calculates a Maximum General Unificator for a list of terms if it exists.

atomsMGU : FormulaFOL -> FormulaFOL -> Maybe Substitution

It calculates a Maximum General Unificator for two atoms if it exists.

Modules