Symbolic Computation and Symbolic Computing Grid Based on the Interaction of Provers, Solvers and Reduces

该研究项目的目标有两个方面：（1）探索验证软件和描述形式对象属性的语句的方法，例如基于Buchberger观察到的证明器，求解器和归约器的交互原理的数学定理和Web文档;（2）实现能够探索这些方法的符号计算网络。关于第一个目标，我们已经成功地产生了各种结果的计算机辅助验证的几何定理，特别是定理折纸建设和验证动态生成的Web文档。关于第二个目标，我们开发了一个软件系统，称为Scorum（符号计算研究论坛），在Web上提供符号计算服务。Scorum是使用GWT（Google Web Toolkit）和Web服务技术构建的。使用Scorum，我们成功地自动化证明的一些折纸定理使用Groebner基地理论和理论的圆柱代数分解。

The objectives of this research project are two fold: (1) to explore the methodologies for verifying software and statements describing properties of formal objects such as Mathematical theorems and web documents based on the principles of interactions of provers, solvers and reducers observed by Buchberger and (2) to realize the symbolic computing network that enables the exploration of such methodologies. Concerning the first objective we have successfully produced various results of computer assisted verification of geometrical theorems especially theorems about origami construction and the verification of dynamically generated web documents. Concerning the second objective, we developed a software system call Scorum (Symbolic computation research forum) that offers services of symbolic computation on the web. Scorum was built using GWT (Google Web Toolkit) and using the technology of web services. Using Scorum, we successfully automated proofs of some origami theorems using Groebner bases theory and the theory of cylindrical algebraic decomposition.