Nominal AntiUnification
This is a Java implementation of the antiunification
algorithm for nominal terms described in:
The algorithm solves the following problem:
GIVEN: 
Nominal terms t and s of the same sort, a freshness context ∇ and a finite set of atoms A such that t, s, and ∇ are based on A. 
FIND: 
A term r and a freshness context Γ, such that the termincontext <Γ, r> is an Abased least general generalization of the termsincontext <∇, t> and <∇, s>. 
The antiunification algorithm relies on
a subalgorithm that constructively decides equivariance between
two termsincontext. This subalgorithm can also be
accessed separately.
Input Syntax:

The symbols AZ, az, 19 are allowed for atom names,
function names, variable names and sort names. Names can be of any length.
 If the first letter of the name is within [a,e] or [A,E], then it
is an atom.
 If the first letter of the name is within [u,z] or [U,Z], then it
is a variable.
 Otherwise it is a function symbol. The application of a function with arity zero f() may be written as just f.
 The dot "." is used for abstraction.
 The colon ":" is used to declare the sorts.
 If a sort name starts with a capital letter, then it is of sort data.
 The dash "" is used as type constructor.
 The sharp "#" is used for freshness constrains.
 Mixed mode of typed and untyped calculus is allowed.
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(a,b) =^= f(a,b)
 f(a,a) =^= f(b,b)
 f(a,a) =^= f(b,c)
 f(a,b) =^= f(b,c)
 f(a:i,a:i):o =^= f:iio(b,b)
 a.a =^= b.c
 a.b =^= b.a
 a.b =^= b.a with extra atom c
 f(a,b) =^= f(Y,(a b)Y) with nabla {b#Y}
 f(b,a) =^= f(Y,(a b)Y) with nabla {b#Y}
 h(a.a, b.b) =^= h(c.Y, c.Y) with nabla {a#Y}
 h(f(X1), c.f(X1)) =^= h(g(X2), c.g(X2)) with nabla {c#X1, c#X2}
 h(f(X1), a.f((a c)X1)) =^= h(g(X2), b.g((b c)X2)) with nabla {a#X1,b#X1,c#X1,a#X2,b#X2,c#X2}
 h(f(X1), a.f(X2)) =^= h(g(X1), a.g(X2)) with nabla {a#X1}
 a.b.c =^= c.a.b
 a.b.b =^= b.b.a
 f(a.b, X) =^= f(b.a, Y) with nabla {c#X}

