Re: [Hol-info] Bug in REAL_SOS?

[John H. <Joh...@cl...>]

Hi Steve,

| 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

This seems to be another case of the bug you identified earlier:
REAL_SOS just doesn't know that injections of naturals (in this
case "&p") are always nonnegative. I'll make sure these cases work
when I fix the bug.

| 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.

This is probably because the interrupt hits the semidefinite
programming engine itself. The temporary file is created by that,
and then read in by HOL.

John.