|
From: Stephen B. <ste...@ve...> - 2006-06-26 07:04:49
|
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 |