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

2001 Fiscal Year Annual Research Report

• Project/Area Number: 13224088
• Research Institution: National Institute of Informatics
• Principal Investigator: 佐藤 健 国立情報学研究所, 情報学基礎研究系, 教授 (00271635)
• Co-Investigator(Kenkyū-buntansha): 新井 紀子 国立情報学研究所, 情報学基礎研究系, 助教授 (40264931) ; 龍田 真 国立情報学研究所, 情報学基礎研究系, 教授 (80216994)
• Keywords: ソフトウェア発展 / 極小更新 / 仮説論理プログラム / 宣言的プログラミング

Research Abstract

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

Research Products

• [Publications] Satoh, K.: "Computing Minimal Belief Revision by Extended Logic Programming without Minimality Check'"Proc. of IJCAI-01 Workshop on Abductive Reasoning. 48-55 (2001)
• [Publications] 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)
• [Publications] Arai, N., Pittassi, T., Urquhart, A.: "The complexity of analytic tableaux"Proceedings of STOC2001 (Symposium of Theory of Computing). 356-363 (2001)
• [Publications] 岩山 登, 佐藤 健: "論理プログラムの解集合意味論に関する証明系"人工知能学会誌. 16・5. 665-660 (2001)