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

点击翻译按钮获取中文摘要

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.