Hi Madalina,
| 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).
I think this may just be a typing issue. Note that numerals are
interpreted as natural numbers (type :num) rather than reals, and
this gives all your subexpressions type :num as well. Your problem
should work if you use the natural number version SOS_RULE:
SOS_RULE
`a1>=0 /\ a2>=0 /\
(a1*a1 + a2*a2 = b1*b1 +b2*b2 +2) /\
(a1*b1 + a2*b2 = 0)
==> a1*a2 -b1*b2 >= 0`;;
or if you explicitly make the type :real, adding the type coercion
"&" to numerals:
REAL_SOS
`a1:real >= &0 /\ a2 >= &0 /\
(a1*a1 + a2*a2 = b1*b1 +b2*b2 + &2) /\
(a1*b1 + a2*b2 = &0)
==> a1*a2 - b1*b2 >= &0`;;
| I wonder what is wrong because both tactics use CSDP. I meantion that
| I have installed the version of Ocaml from 10.01.2010.
In principle there can be differences depending on the CSDP version,
the linear algebra subroutines underneath it etc. However, this seems
quite rare; I've only encountered it once.
John.
------------------------------------------------------------------------------
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
