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.
Input Syntax:
-
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
function symbol.
- 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").
For presentation purpose, the Java source code has been translated into JavaScript by the
GWT compiler.
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)
|
|