7812032 的博客

日志

关于我

华三火

文章分类

·默认分类（944）

【原创】执着的追求，勇敢的探索——简介刘保乾的专著《BOTTEMA—我们看见了什么》（续）

2009-11-05 22:39:52| 分类：默认分类 | 标签： |举报 |字号大中小订阅

下载LOFTER 我的照片书 |

刘先生在《BOTTEMA—我们看见了什么》一书（以下简称BO—书）中第一章叙述了BOTEMA软件（以下简称B—软件）的基本功能、使用技巧和指出一个不等式在给出机器证明后若能再给出可读的人工证明才是和谐和完美的。B—软件一个重要功能是能够确定不等式的最佳系数，这个最佳系数常常是机器证明中所给出的一个代数方程的根。这里举出书中的一个例子说明：（阅读以下内容需一定的数学知识）

［例1] 1971年，M.S.Klamkin曾建立过一个关于三角形ABC三边a、b、c的轮换对称不等式

∑(a/b)≥(1/3)*∑a*∑（1/a) (1)

考虑差式 ∑(a/b)-(1/3)*∑a*∑a*∑(1/a) 与差式 ∑(a/b)-3的比较，有

K*(∑(a/b)-3)≥∑(a/b)-(1/3)*∑a*(1/a)≥K＇*(∑(a/b)-3)

（2)

其中K,K'是方程 1863*K＾4-2646*K＾3+1449*K^2-354*K+31=0的两实根，K=0.428996848…，K'=0.1991646838…。

上面的结果即为运用B—软件所证明的结果，其中系数K,K'最佳。这与福建陈胜利老师得到的可读性证明结果

K=[sqrt(13+16*sqrt2)+3]/[(3*sqrt(13+16*sqrt2)+1]

=0.428996848…

K'=[sqrt(13+16*sqrt2-3]/[3*sqrt(13+16*sqrt2)-1]

=0.1991646838…

是一致的。

该章最后还举例说明了目前机器证明和人工推理证明各有特色也各有不足之处。

BO—书第二章由中国科学院计算技术研究所夏时洪博士撰写。系统地介绍了B—软件的原理和算法。夏博士首先回顾了自1977年吴文俊院士创立了机械化的吴法，1992年张景中院士用自己创造的消点算法在计算机上实现了可读性证明，初等几何有关等式型定理的机器证明基本解决。1996年以来，杨路教授及其合作者的研究表明代数方程的判别系统的研究进展说明能够用于不等式的证明。直至杨路教授提出一个全新的算法—降维算法，成功地降低维数又可消去根式这一问题，从而基本解决初等几何不等式和更大一类附加某些条件的代数不等式的机器证明问题。然后介绍了杨路方法的原理和算法。并指出应用B-软件来证明数学家Bottema等人的专著《几何不等式》中的100个基本不等式总共用的时间为5秒左右。B—软件在证明不等式时的效率之高是十分惊人的。（注：杨路教授为了纪念在几何不等式研究领域中有重要贡献的数学家Bottema，才将自己创新的软件取名BOTTEMA软件）

（未完待续）

评论这张

转发至微博

阅读(219)| 评论(3)

历史上的今天

this.p={  m:2,
              b:2,
              loftPermalink:'',
              id:'fks_083066081087084075092082086095085084086068087083086065092',
              blogTitle:'【原创】执着的追求，勇敢的探索——简介刘保乾的专著《BOTTEMA—我们看见了什么》（续）',
              blogAbstract:'<P\><FONT color=#000000 size=3\><STRONG\><EM\></EM\></STRONG\></FONT\> <STRONG\><EM\><FONT color=#000000 size=3\>      <FONT face=黑体\>刘先生在《BOTTEMA—我们看见了什么》一书（以下简称BO—书）中第一章叙述了BOTEMA软件（以下简称B—软件）的基本功能、使用技巧和指出一个不等式在给出机器证明后若能再给出可读的人工证明才是和谐和完美的。B—软件一个重要功能是能够确定不等式的最佳系数，这个最佳系数常常是机器证明中所给出的一个代数方程的根。这里举出书中的一个例子说明：（阅读以下内容需一定的数学知识）</FONT\></FONT\></EM\></STRONG\></P\>\r\n<P\><STRONG\><EM\><FONT face=黑体 size=3\>         ［例1]  1971年，M.S.Klamkin曾建立过一个关于三角形ABC三边a、b、c的轮换对称不等式</FONT\></EM\></STRONG\></P\>\r\n<P\><STRONG\><EM\><FONT face=黑体 size=3\>   </FONT\></EM\></STRONG\></P\>',
              blogTag:'',
              blogUrl:'blog/static/127735028200910510294757',
              isPublished:1,
              istop:false,
              type:0,
              modifyTime:1265983696446,
              publishTime:1257431992075,
              permalink:'blog/static/127735028200910510294757',
              commentCount:3,
              mainCommentCount:2,
              recommendCount:1,
              bsrk:-100,
              publisherId:0,
              recomBlogHome:false,
              currentRecomBlog:false,
              attachmentsFileIds:[],
              vote:{},
              groupInfo:{},
              friendstatus:'none',
              followstatus:'unFollow',
              pubSucc:'',
              visitorProvince:'',
              visitorCity:'',
              visitorNewUser:false,
              postAddInfo:{},
              mset:'000',
              mcon:'',
              srk:-100,
              remindgoodnightblog:false,
              isBlackVisitor:false,
              isShowYodaoAd:false,
              hostIntro:'',
              hmcon:'1',
              selfRecomBlogCount:'0',
              lofter_single:'<iframe width="140" height="560" style="overflow:hidden;" src="http://www.lofter.com/mailEntry.do?blogad=1&blog" frameBorder="0"></iframe>'
            }

{list a as x}
    {if !!x}
    <div class="iblock nbw-fce nbw-f40">
      <a class="fc03 noul" target="_blank" hidefocus="true" href="http://blog.163.com/${x.visitorName}/">
      {if x.visitorName==visitor.userName}
      <img alt="${x.visitorNickname|escape}" onerror="this.src=location.f40" class="cwd bdwa bdc0" src="${fn1(x.visitorName)}&r=${visitor.imageUpdateTime}"/>
      {else}
      <img alt="${x.visitorNickname|escape}" onerror="this.src=location.f40" class="cwd bdwa bdc0" src="${fn1(x.visitorName)}"/>
      {/if}
      </a>
      <div class="cwd vname thide">
        {if x.moveFrom=='wap'}
          <a class="noul pnt" target="_blank" href="http://blog.163.com/services/wapblog.html?frompersonalbloghome"><span title="来自网易手机博客" class="iblock wapIcon"> </span></a>
        {elseif x.moveFrom=='iphone'}
          <a class="noul pnt" target="_blank"><span title="来自iPhone客户端" class="iblock iphoneIcon"> </span></a>
        {elseif x.moveFrom=='android'}
          <a class="noul pnt" target="_blank"><span title="来自Android客户端" class="iblock androidIcon"> </span></a>
        {elseif x.moveFrom=='mobile'}
          <a class="noul pnt" target="_blank" href="http://blog.163.com/services/emsblog.html?frompersonalbloghome"><span title="来自网易短信写博" class="iblock wapIcon"> </span></a>
        {/if}
        <a class="fc03 m2a"  target="_blank" hidefocus="true" href="http://blog.163.com/${x.visitorName}/">
          ${fn(x.visitorNickname,8)|escape}
        </a>
      </div>
    </div>
    {/if}
    {/list}

<#--最新日志，群博日志--> <#--推荐日志-->

<p class="fc06">推荐过这篇日志的人：</p>
    <div>
      {list a as x}
      {if !!x}
      <div class="iblock nbw-fce nbw-f40">
        <a class="fc03 noul" target="_blank" hidefocus="true" href="http://blog.163.com/${x.recommenderName}/">
        <img alt="${x.recommenderNickname|escape}" onerror="this.src=location.f40" class="cwd bdwa bdc0" src="${fn1(x.recommenderName)}"/>
        </a>
        <div class="cwd thide">
          <a class="fc03 m2a" target="_blank" hidefocus="true" href="http://blog.163.com/${x.recommenderName}/">
            ${fn(x.recommenderNickname,6)|escape}
          </a>
        </div>
      </div>
      {/if}
      {/list}
    </div>
    {if !!b&&b.length>0}
    <p  class="fc06">他们还推荐了：</p>
    <ul>
    {list b as y}
      {if !!y}
        <li class="rrb"><span class="iblock">·</span><a class="fc03 m2a" target="_blank" href="http://blog.163.com/${y.recommendBlogPermalink}/?from=blog/static/127735028200910510294757">${y.recommendBlogTitle|escape}</a></li>
      {/if}
    {/list}
    </ul>
    {/if}

<#--引用记录--> <#--博主推荐--> <#--随机阅读--> <#--首页推荐--> <#--历史上的今天--> <#--被推荐日志--> <#--上一篇，下一篇--> <#-- 热度 -->

{list a as x}
    {if !!x}
    <div class="hotItem iblock nbw-fce nbw-f40">
      <a class="fc03 noul" target="_blank" hidefocus="true" href="http://blog.163.com/${x.publisherUsername}/">
      {if x.publisherUsername==visitor.userName}
      <img alt="${x.publisherNickname|escape}" onerror="this.src=location.f40" class="cwd bdwa bdc0" src="${fn1(x.publisherUsername)}&r=${visitor.imageUpdateTime}"/>
      {else}
      <img alt="${x.publisherNickname|escape}" onerror="this.src=location.f40" class="cwd bdwa bdc0" src="${fn1(x.publisherUsername)}"/>
      {/if}
      </a>
      <div class="cwd vname thide">
        <a class="fc03 m2a"  target="_blank" hidefocus="true" href="http://blog.163.com/${x.publisherUsername}/">
          ${fn(x.publisherNickname,8)|escape}
        </a>
      </div>
      <a class="f-myLikeIcons hottype {if x.type==1} js-liketype{elseif x.type==2} js-reblogtype{elseif x.type==3} js-sharetype{else}{/if}" target="_blank" hidefocus="true" href="http://blog.163.com/${x.publisherUsername}/"> </a>
    </div>
    {/if}
    {/list}

<#-- 网易新闻广告 --> <#--右边模块结构--> <#--评论模块结构--> <#--引用模块结构--> <#--博主发起的投票-->

页脚

我的照片书 - 手机博客 - 下载LOFTER APP - 订阅此博客

7812032 的博客

导航

日志

【原创】执着的追求，勇敢的探索——简介刘保乾的专著《BOTTEMA—我们看见了什么》（续）

历史上的今天

最近读者

热度

评论

页脚