Anti-Unification for Unranked Terms and Hedges

This is a Java implementation of the algorithm G(R) described in:

Temur Kutsia, Jordi Levy, Mateu Villaret. Anti-Unification for Unranked Terms and Hedges.
Journal of Automated Reasoning, 52(2): 155-190, 2014.

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.

Anti-unification problem: (Use the semicolon to separate the equations of the system. Hedge equations are allowed.)	( f(a,b,c), g(a) ) =^= ( f(a,b,a,c), g(a), h(b) )
Rigidity function:
Minimum alignment length:
Iterate all possibilities:
Output format:

Your web browser must have JavaScript enabled in order for this application to work.

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(a,a), a, X, b) =^= f(g(b,b), g(Y), b)
(f(a), f(a)) =^= (f(a), f)
if(geq(x1, x2), then(eq(x3, add(x4, x2)), eq(x4, add(x4, 1))), else(eq(x3, sub(x4, x1)))) =^=
if(geq(y1, y2), then(eq(y3, add(y4, y2)), eq(y5, 1), eq(y4, add(y4, 5))), else(eq(y3, sub(y4, y1))))
a, a, b, f, f, f(a, a, b) =^= a, a, c, f, f, f(a, a, c)
a, a, b, b, f, f, f(a, a, b, b) =^= a, a, c, f, f, f(a, a, c)
f(g(a, X), a, X, b) =^= f(g(b), b))

Author:	Alexander Baumgartner
Project:	SToUT - Symbolic Computation Techniques for Unranked Terms