Unification for Unranked Terms with Sequence Variables
This is a Java implementation of the algorithm ULight without sequence functions described in:
Part of the Library of Unification and Anti-Unification Algorithms.
The symbols [A-Za-z1-9_.] are allowed for variable names and
function names. Names can be of any length.
- If the name is followed by an opening parenthesis, then it is a
- Otherwise, if the name starts with an upper case letter, then it is
a hedge variable.
- Otherwise, if the first letter of the name is within [u,z], then it
is a term variable.
- Otherwise, the name is a constant.
This software is released under the GNU Lesser General Public License ("LGPL")
Some examples (click on them to prepared the input form):
- f(g(x,b), X, b) =? f(g(y,x), g(a), b, b)
- f(X, x, Y) =? f(f(X), x, a, b)