NOTE: the latest version is 10.1.0

Unavailable. Nobody can download this version any more, with elm or with the Lamdera compiler: github.com/vicramgon/logicus is gone (deleted or private); Software Heritage not asked yet (this run's --swh-calls were used up); no fork with tag 7.0.0 found (12 same-name repos checked); no cached copy. Use another version.

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

Propositional Logic

First Order Logic