宣言的プログラミングにおけるソフトウェア発展の研究

声明式编程中的软件开发研究

• 批准号: 13224088
• 负责人: 佐藤 健
• 金额: --
• 依托单位: National Institute of Informatics
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas (C)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13224088/
• 关键词: ソフトウェア発展; 極小更新; 仮説論理プログラム; 宣言的プログラミング

ソフトェア発展はソフトウェア科学およびソフトウェア工学における重要なテーマである。佐藤は、以前、特定領域研究「発展機構を備えたソフトウェアの構成原理の研究」において極小変更の考えを用いたソフトウェア仕様の変更の研究を行い、仮説論理プログラミングによるプロトタイプシステムの開発も行った。本研究は、その研究をさらに発展させ、論理型プログラミングや関数型プログラミングのような宣言的なプログラミングに通用する,より一般的なソフトウェア発展の理論を構築することを目的とするものである.今年度では,このための基礎的な準備として以下の研究を行った.佐藤は,関数のない論理仕様に対する極小変更の自動化に向けて論理仕様を仮説論理型プログラムに変換し,その上での処理系で極小変更が自動的に行えるクラスの同定を行った.さらに,論理仕様に矛盾が生じたときに,その矛盾の一般化を用いて,より適切な更新ができるように,PAC learningの枠組みに基づいた極大矛盾除去の手法の検討を行った.龍田は,直観主義論理に基づく構成的なプログラム合成の研究において,二階古典自然演繹の強正規化性に関してCPS変換を用いたParigotの証明の誤りを指摘し,その原因であるCPS変換の継続消滅について論じ,オグメンテーションの概念を用いて証明を完成させた.新井は,命題論理の証明の複雑さについて,自動証明で頻繁に用いられるresolutionシステムとtableauxシステムの効率比較を理論的に行い,さらに、両システムを融合し新しい推論規則(symmetry rule)を導入したシステムの実装を行い,ここで初等的な組み合わせ論の問題を短時間で解くことに成功した.

I don't know. I don't know what to do. Sato, in the past, and in specific fields, the exhibition organization has studied the principle of research in the field of science and technology. The purpose of this study is to study the general situation of the manifesto, the general theory and the purpose of this study. In the current year, we will prepare for the following research projects. Sato Yoshimi, the number of people in the department of science, and the department of science. In general, in general, In the study of the synthesis of CPS, which is based on the theory of science and technology, the classical natural evolution is strongly standardized and the CPS is used to criticize the errors. The reason is that the reason is not correct, and that the concept is used to complete the experiment. In the new well, the mission theory shows that there is a copy of the computer, the automatic simulation shows that the failure rate of the resolution is higher than that of the theoretical theory, and that the rules of the new reasoning (symmetry rule) are incorporated into the software assembly line, and that the elementary combination of computer problems is successfully solved in a short time.

项目成果

岩山 登, 佐藤 健: "論理プログラムの解集合意味論に関する証明系"人工知能学会誌. 16・5. 665-660 (2001)

Noboru Iwayama，Ken Sato：“逻辑程序解集语义的证明系统”日本人工智能学会杂志 16・5（2001 年）。

Satoh, K.: "Computing Minimal Belief Revision by Extended Logic Programming without Minimality Check'"Proc. of IJCAI-01 Workshop on Abductive Reasoning. 48-55 (2001)

Satoh, K.：“通过扩展逻辑编程计算最小置信修正，无需最小性检查”Proc。

Arai, N., Masukawa, R.: "How to find symmetries hidden in combinatorial problems, pp18-32 in Symbolic Computation and Automated Reasoning, ed."M. Kerber and M. Kohlhase, A K Peters eds., Symbolic Computation and Automated Reasoning. 18-32 (2001)

Arai, N.，Masukawa, R.：“如何找到隐藏在组合问题中的对称性，《符号计算和自动推理》第 18-32 页，编辑。”M.

Arai, N., Pittassi, T., Urquhart, A.: "The complexity of analytic tableaux"Proceedings of STOC2001 (Symposium of Theory of Computing). 356-363 (2001)

Arai, N.、Pittassi, T.、Urquhart, A.：“分析画面的复杂性”STOC2001（计算理论研讨会）论文集。