Menu
▾
▴
Re: [Hol-info] Bug in REAL_SOS?
|
From: <Mal...@cs...> - 2006-06-26 09:29:44
|
Stephen Brackin writes: > 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 > > > > <html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns="http://www.w3.org/TR/REC-html40"> > > <head> > <meta http-equiv=Content-Type content="text/html; charset=us-ascii"> > <meta name=Generator content="Microsoft Word 11 (filtered medium)"> > <style> > <!-- > /* Style Definitions */ > p.MsoNormal, li.MsoNormal, div.MsoNormal > {margin:0in; > margin-bottom:.0001pt; > font-size:12.0pt; > font-family:"Times New Roman";} > a:link, span.MsoHyperlink > {color:blue; > text-decoration:underline;} > a:visited, span.MsoHyperlinkFollowed > {color:purple; > text-decoration:underline;} > pre > {margin:0in; > margin-bottom:.0001pt; > font-size:10.0pt; > font-family:"Courier New";} > span.EmailStyle17 > {mso-style-type:personal-compose; > font-family:Arial; > color:windowtext;} > @page Section1 > {size:8.5in 11.0in; > margin:1.0in 1.25in 1.0in 1.25in;} > div.Section1 > {page:Section1;} > --> > </style> > > </head> > > <body lang=EN-US link=blue vlink=purple> > > <div class=Section1> > > <p class=MsoNormal><font size=2 face="Courier New"><span style='font-size:10.0pt; > font-family:"Courier New"'>I’ve found what seems to be a bug in HOL Light’s > REAL_SOS. It didn’t prove<o:p></o:p></span></font></p> > > <p class=MsoNormal><font size=2 face="Courier New"><span style='font-size:10.0pt; > font-family:"Courier New"'><o:p> </o:p></span></font></p> > > <pre><font size=2 face="Courier New"><span style='font-size:10.0pt'>`&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &p + -- &1 * &q > &0` or<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>`&q >= &1 /\ &p pow 2 = &2 * &q pow 2 ==> &2 * &q - &p < &p`<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>In several minutes, although SOS_RULE proved the corresponding “for naturals” statements<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>`q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> p - 1 * q > 0` and<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>`q >= 1 /\ p EXP 2 = 2 * q EXP 2 ==> 2 * q - p < p`<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>in seconds. Getting rid of the natural numbers altogether didn’t help; REAL_SOS also couldn’t prove either of<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>`q >= &1 /\ p pow 2 = &2 * q pow 2 ==> p + -- &1 * q > &0` or<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>`q >= &1 /\ p pow 2 = &2 * q pow 2 ==> &2 * q - p < p`.<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>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.<o:p></o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'><o:p> </o:p></span></font></pre><pre><font > size=2 face="Courier New"><span style='font-size:10.0pt'>Steve Brackin<o:p></o:p></span></font></pre> > > <p class=MsoNormal><font size=2 face="Courier New"><span style='font-size:10.0pt; > font-family:"Courier New"'><o:p> </o:p></span></font></p> > > </div> > > </body> > > </html> > Using Tomcat but need to do more? Need to support web services, security? > Get stuff done quickly with pre-integrated technology to make your job easier > Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo > http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642 > _______________________________________________ > hol-info mailing list > hol...@li... > https://lists.sourceforge.net/lists/listinfo/hol-info |
