# Unranked Second-Order Anti-Unification

This is a Java implementation of the algorithm described in:

Input Syntax:
• The symbols [a-zA-Z1-9_.] are allowed for variable names and function names. Names can be of any length.
• If the first letter of the name is within [u-zU-Z], then it is a variable.
• If the variable is applied to a hedge then it is a context variable (e.g. X(a, b)).
• Otherwise, it is a hedge variable (e.g. f(x, a)).
• Otherwise, it is a function symbol.
• The input hedges have to be variable disjoint.
 Anti-unification problem:(Use the semicolon to separate the equations of the system.Hedge equations are allowed.) f(c), f(f(g(a, a)), a, a) =^= c, f(g(b, b, b), b, b, b) Alignment computation: Compute longest admissible alignments. Longest admissible alignments are computed by computing common subsequences of the word representation of the input hedges. Therefore all the longest common subsequences (in form of alignments) with respect to a given upper bound are tested for admissibility. If none of them is admissible, then the upper bound is reduced. Input an alignment by hand. e.g. a<1.1, 2.2> f<2, 3> a<2.1.2, 3.1> Justify computed generalization: By obtaining substitutions from the store, instantiating the generalization and comparing the result with the input. Iterate all possibilities: Compute generalizations for all admissible alignments, or only for the first one. Output format: SimpleVerboseProgress

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, g(h(a, h(b)))) =^= f(a, a, h(g(b))) f(g(a,a), a, X, b) =^= f(g(b,b), g(Y), b) f(h(c,a,c,a), a, a) =^= f(g(c,b,c,a), b, b) f(x), f(f(g(a,a)), a, a) =^= x, f(g(b,b), b, b) f(x), f(f(g(a,a)), a, a) =^= x, f(g(b,a), a, b) f(x), f(h(f(c,a)), a, c) =^= x, f(g(b,a), a, 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)) a,a,a,a,a,a,a,a,a,a,a,a =^= a,a,a,a,a,a,a,a,a,a

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