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.
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
