[Hol-info] Bug in REAL_SOS?

[Stephen B. <ste...@ve...>]

I've found what seems to be a bug in HOL Light's REAL_SOS. It didn't prove

 

`&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &p + -- &1 * &q > &0` or
`&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &2 * &q - &p < &p`
 
In several minutes, although SOS_RULE proved the corresponding "for
naturals" statements
 
`q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> p - 1 * q > 0` and
`q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> 2 * q - p < p`
 
in seconds.  Getting rid of the natural numbers altogether didn't help;
REAL_SOS also couldn't prove either of
 
`q >= &1 /\ p pow 2 = &2 * q pow 2 ==> p + -- &1 * q > &0` or
`q >= &1 /\ p pow 2 = &2 * q pow 2 ==> &2 * q - p < p`.
 
When I interrupted the REAL_SOS proof attempts, I sometimes got an error
message such as Sys_error "/tmp/sosfsbc40.out: No such file or directory",
but other times not.
 
Steve Brackin