对外合作项目：几何自动推理软件－JGEX的开发

JGEX（全名Java Geometry Expert，或者Java版几何专家）是基于早期的GEX(几何专家)。几何专家软件最初的开发于1994年，主要的开发者有： 周咸青，美国Wichita州立大学教授，浙江大学客座教授 高小山，首席科学家， 中科院系统所所长 张景中，中国科学院院士

JGEX的开发开始于2004年在美国Wichita 州立大学，目前最新的版本是0.70。JGEX 是一个集几何作图，证明，推理的软件，它是基于吴文俊先生所提出的“吴方法”以及随后发展的一些列自动证明方法：全角法，面积法，Groebner Basis方法，演绎数据库法等。 JGEX目标：　将几何中的基本问题自动化，几何定理的自动证明，几何定理与公式的自动发现，几何图形的自动生成 目标：通过我们软件，使得几何问题可以有效，快速得到解决。如果需要更多的详细资料，请访问我们的网站：http://woody.cs.wichita.edu

后续开发计划：1）传统的可读证明的产生。我们准备在JGEX中加入产生传统的证明功能。这是一个非常有意义和挑战性的问题，目前国际上对这个领域的研究还停留在初始阶段。 2）Proof Check，证明验证。这是一个非常大的领域，我们准备做的只是几何证明的验证；3）几何定理辅助线的自动生成。几何的辅助线是在证明过程中非常重要的一环，我们希望能通过总结解几何题目的经验，结合人工智能的方法，在自动添加辅助线这个方面迈出一大步。 JGEX是由Wichita州立大学自动证明小组开发，它的开发是受到美国国家自然科学基金(NSF)的资助（CCR-0201253）。由于自动证明小组的杰出贡献，NSF已经连续资助他们的研究将近20年。在国内，我们也受到中国国家自然科学基金的支持，并且，我们和中国科学院系统科学研究所有良好的合作关系。吴文俊先生就是原系统科学研究所所长，数学机械化中心主任。

图. 界面演示