Re: [Hol-info] Bug in REAL_SOS?

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

I'd guess that it's NOT the same bug, because of the last thing I mentioned
in my first Hol-info note on this: Replacing &p and &q by p and q,
re-defining p and q as real rather than natural-number variables, didn't
help.

I had a thought that might be helpful: Wouldn't it make things faster to
have the SOS functions first normalize their inputs using the same sort of
algorithm REAL_FIELD uses, and then continue with the sum-of-squares stuff?
That would make them almost as fast as REAL_FIELD on the cases REAL_FIELD
can handle, and it will probably speed things up on the other cases, too.

Steve

> -----Original Message-----
> From: John Harrison [mailto:Joh...@cl...]
> Sent: Monday, June 26, 2006 11:42 AM
> To: Stephen Brackin
> Cc: hol...@li...
> Subject: Re: [Hol-info] Bug in REAL_SOS?
> 
> 
> 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.