您好,欢迎来到国际技术转移服务平台!请先登录 或者 免费注册
张景中
  • 信用等级: 0
  • 手机:13880522699
  • 邮件:zjz1936@126.com
  • 所在地区:中国
(www.kj01.cn)

他的关注

  • 潘复生
  • 重庆理工大学汽车
  • 重庆市前沿专利事
  • 重庆科技检测中心
  • 重庆生产力促进中
  • 石晓辉
  • 胡远志
  • 朱新才
  • 重庆低碳研究中心

几何定理机器证明理论与算法的新进展

  • 商品售价:面议
  • 技术类型:新技术/新工艺/其他
  • 所属行业:其他 
  • 成 熟 度 :完成研发
  • 技术水平:国内领先
  • 合作方式:合作研发
  • 留言信息:(0)
关键字: 计算机

技术成果简介

(一)创立计算机生成几何定理可读证明的原理与算法能否用计算机产生几何定理的可读证明(即入容易理解和检验的证明),是人工智能领域的一大难题。该成果研究人员提出以消点思想为主线的新原理,给出了世界上第一个能够自动产生几何定理可读证明的算法和程序。不仅给出的证明简短可读,效率也比已知其它算法高得多。随即将消点思想运用于非欧几何,给出世界上第一个非欧几何可读证明自动生成程序,从而开创了靠计算机通用程序成发现非平凡新定理的先例。这一成果使得机器证明的研究从以判定为主的阶段进入机器产生的证明与人的手工证明竞相比美的阶段。被国际著名计算机科学家R.BOYER誉为“自动推理领域三十年来最重要的工作”,“发展计算机处理几何问题能力的道路上的里程碑”。

(二)创立定理机器证明的数值并行方法的原理与算法该成果研究人员提出了对给定的命题通过有限次数值检验加以严格证明的有效算法。在国际上首次实现了用低档微机证明非平凡几何定理以及发现新定理。该算法也是目前唯一可并行的几何定理机器证明算法。

(三)对几何定理机器证明的方法的改进与发展创建“含参结式法”,“WR分解”,“聚筛法”等有效算法;建立了文字系数多项式的完全判别系统,为不等式的快速证明提供了有力工具。

合作案例

渝ICP备09050127号-5