Singleton Tree Grammars (STGs) have recently drawn considerable#R##N#attention. They generalize the sharing of subtrees known from DAGs to#R##N#sharing of connected subgraphs. This allows to obtain smaller#R##N#in-memory representations of trees than with DAGs. In the past years#R##N#some important tree algorithms were proved to perform efficiently#R##N#(without decompression) over STGs; e.g., type checking, equivalence#R##N#checking, and unification. We present a tool that implements an#R##N#extension of the unification algorithm for STGs. This algorithm makes#R##N#extensive use of equivalence checking. For the latter we implemented#R##N#two variants, the classical exact one and a recent randomized one. Our#R##N#experiments show that the randomized algorithm performs better.  The#R##N#running times are also compared to those of unification over#R##N#uncompressed trees.
['Adrià Gascón', 'Sebastian Maneth', 'Lander Ramos']
First-Order Unification on Compressed Terms