[Termtools] [color] unification

[Frederic Blanqui]

I cannot test this new feature on a large scale now. So it's up to you...

By the way, I'm afraid that the tools based on Rainbow/CoLoR are not 
going to be very good in this competition. The last months have not been 
a very good time for Adam and I to work on this: Adam finished his PhD 
and I moved to China. So various important improvements are not finished 
yet, and the proofs using <scc_decomp> often cannot be checked at all 
(it takes too much time). It means that it is better not to use 
<scc_decomp> whenever possible, otherwise you will get results worse 
than the last competition. And the <decomp> proof node which is intended 
to replace <scc_decomp> is not completely working yet. I would need a 
few days more...



Ulrich Schmidt-Goertz a écrit :
> Frederic Blanqui schrieb:
>> Dear all, it is now possible to use graph approximation based on
>> unification in Rainbow and CoLoR (tag <unif> instead of <hde>).
>>
>> (To this end, I had to prove the termination, correctness and
>> completeness of some unification algorithm.)
> 
> Nice. Is this ready to be used in the competition (and if yes, do we
> want to use it on such a short notice)?
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools