unification is a concrete implementation of logical first-order unification
and library to apply a first-order unification procedure
unify given by the library
on two terms of
Termtype given by the library.
A solution of a unification problem is a substitution, that is, a mapping assigning a symbolic value to each variable of the problem's expressions. The unification algorithm reports unsolvability for a given problem or computes a complete, and minimal singleton substitution set containing the so-called most general unifier, that is, a set covering all its solutions, and containing no redundant members.
import "package:tailcalls/tailcalls.dart"; import "package:unification/unification.dart"; var test = unify( new List() ..add( new Tupl( new Term("b0", [new Term("b1", ),new Term("b2", )]), new Term("b0", [new Term("b1", ),new Term("b2", )]), ), ), ).result(); var mgu = test; print(mgu.toString());
Read more about unification in logic on Wikipedia.