| Project/Area Number |
17300004
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
IDA Tetsuo University of Tsukuba, Graduate School of Systems and Information Engineering, Professor (70100047)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
MINAMIDE Yasuhiko University of Tsukuba, Graduate School of Systems and Information Engineering, Associate Professor (50252531)
MIRCEA Marin University of Tsukuba, Graduate School of Systems and Information Engineering, Associate Professor (60396603)
|
|---|
| Project Period (FY) |
2005 – 2007
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥11,600,000 (Direct Cost: ¥10,700,000、Indirect Cost: ¥900,000)
Fiscal Year 2007: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2006: ¥3,600,000 (Direct Cost: ¥3,600,000)
Fiscal Year 2005: ¥4,100,000 (Direct Cost: ¥4,100,000)
|
|---|
| Keywords | automated theorem proving / software verification / symbolic computation / computational origami / web services / web software / rewrite systems / solvers / ソフトウェア検証 / 計算折り紙 / ウェブソフトウェアシステム / ソフトウェア学 / 情報基礎 / グリッド / グロブナー基底 / 知識処理 |
|---|
| Research Abstract |
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.
|
