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

基于证明者、求解者和约简交互的符号计算和符号计算网格

• 批准号: 17300004
• 负责人: IDA Tetsuo
• 金额: $ 7.42万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2005
• 资助国家: 日本
• 起止时间: 2005 至 2007
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17300004/
• 关键词: automated theorem proving; software verification; symbolic computation; computational origami; web services; web software; rewrite systems; solvers; ソフトウェア検証; 計算折り紙; ウェブソフトウェアシステム; ソフトウェア学; 情報基礎; グリッド; グロブナー基底; 知識処理

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.

该研究项目的目标是两个方面：（1）探索用于验证软件的方法和陈述的方法，描述了基于掠夺者，求解器和重还原的相互作用的原理，诸如数学定理和Web文档之类的属性，由Buchberger和Buchberger和Buchberger and Reducers的相互作用原理（2）实现可以探索此类方法的符号计算网络。关于第一个目标，我们成功地产生了对计算机辅助验证几何定理的各种结果，尤其是关于折纸结构的定理和动态生成的Web文档的验证。关于第二个目标，我们开发了一个软件系统呼叫Scorum（符号计算研究论坛），该Scorum在网络上提供符号计算服务。 Scorum是使用GWT（Google Web Toolkit）和Web服务技术构建的。使用Scorum，我们使用Groebner碱理论和圆柱代数分解理论成功地自动化了某些折纸定理的证据。

项目成果

Analysis of Layers of Feces in Computational Origami Modeling

计算折纸模型中粪便层的分析

• 发表时间: 2007
• 作者: Fadoua;Ghourabi・Hidekazu;Takadashi・Tetsuo;Ida
• 通讯作者: Ida

Foundations of the Rule-based System ρLog

基于规则的系统 ρLog 的基础

• 发表时间: 2006
• 期刊: Journal of Applied Non-Classical Logic 16(1-2)
• 作者: Mircea;Marin・Temur;Kutsia
• 通讯作者: Kutsia

XML Validation for Context-Free Grammars

上下文无关语法的 XML 验证

• 发表时间: 2006
• 期刊: Proc. of The Fourth ASIAN Symposium on Programming Languages and Systems LNCS4279
• 作者: Yasuhiko;Minamide・Akihiko;Tozawa
• 通讯作者: Tozawa

Cプログラムの検証ツールCaduceus(ソフトウェア紹介)

C程序验证工具Caduceus（软件介绍）

• 发表时间: 2007
• 期刊: コンピュータソフトウェア 24
• 作者: 高崎透;中田尚;津邑公暁;中島浩;南出靖彦
• 通讯作者: 南出靖彦

Computational origami environment on the web

• DOI: 10.1007/s11704-008-0009-8
• 发表时间: 2008-03
• 期刊: Frontiers of Computer Science in China
• 作者: Asem Kasem;T. Ida