This is a Java implementation of the algorithm U_{Light} without sequence functions described in:
Part of the Library of Unification and AntiUnification Algorithms.
Input Syntax:
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):

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