RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
about
|
people
|
publications
|
research
|
education
|
industry
|
conferences
|
media
|
projects
internal
  
search:
  

Anti-Unification for Unranked Terms and Hedges

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

Input Syntax:
Anti-unification problem:
(Use the semicolon to separate
the equations of the system.
Hedge equations are allowed.)
Rigidity function:
Minimum alignment length:
Iterate all possibilities:
Output format:

    

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 FWF Der Wissenschaftsfond
Project: SToUT - Symbolic Computation Techniques for Unranked Terms