[Hol-info] Problem with SOS examples in HOL Light

[Madalina E. <me...@ya...>]

Dear HOL Light users,

I'm doing some tests with HOL Light, namely with  the SOS implementation and I have unexpected results (although in the tutorial and in the paper describing the technique the result is different).

For example running:
REAL_SOS `a1>=0 /\ a2>=0 /\ (a1*a1 + a2*a2 = b1*b1 +b2*b2 +2) /\ (a1*b1 + a2*b2 =0) ==> a1*a2 -b1*b2 >= 0`;; 

I get a nonterminating "Searching with depth limit...." 

In contrast the example:

SOS_RULE `1<=x /\ 1 <= y ==> 1<=x*y`;;

has the output expected.

I wonder what is wrong because both tactics use CSDP. I meantion that I have installed the version of Ocaml from 10.01.2010.

Thank you!

Madalina.