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)探索验证软件和描述形式对象（如数学定理和网络文档）属性的方法，该方法基于Buchberger观察到的证明者、求解者和简化者的相互作用原则；(2)实现符号计算网络，使探索这些方法成为可能。关于第一个目标，我们已经成功地产生了计算机辅助验证几何定理的各种结果，特别是关于折纸构造的定理和动态生成的web文档的验证。关于第二个目标，我们开发了一个名为Scorum（符号计算研究论坛）的软件系统，在网络上提供符号计算服务。Scorum是使用GWT （b谷歌Web Toolkit）和Web服务技术构建的。利用Scorum，我们成功地利用Groebner基理论和圆柱代数分解理论自动证明了一些折纸定理。

项目成果

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

Analysis of Layers of Feces in Computational Origami Modeling

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

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

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

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

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

実行可能なコンパイラの形式化と検証

形式化和验证可执行编译器

• 发表时间: 2005
• 期刊: 情報処理学会論文誌:プログラミング No.SIG6(PRO 25)
• 作者: Masanori Hariyama;Naoto Yokoyama;Michitaka Kameyama;Takumi SEIKE;大熊浩示・南出靖彦
• 通讯作者: 大熊浩示・南出靖彦