仮説論理プログラミングを用いたソフトウェア発展モデルの研究

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10139201
• Research Institution: Hokkaido University
• Principal Investigator: 佐藤 健 北海道大学, 大学院・工学研究科, 助教授 (00271635)
• Keywords: 極小変更 / ソフトウェア発展 / 仮説論理プログラミング

Research Abstract

我々は,論理プログラムにおけるソフトウェア発展モデルを研究しており,平成9年度においては,以前,提案した極小変更の定式化を一貫性制約を含む論理プログラムに適用した.平成9年度の研究により,論理プログラミングの変更では,ルール自体の成立/不成立の変更が極小になると考えることが自然であることが分かった.
この結果,論理プログラミングの更新は,元のプログラムのルールをデフォルトルール,一貫性制約を公理と考え,追加されるルールを追加公理と考えたときの式極小限定(Formula Circumscription)に対応することが分かった.さらに論理プログラムの一般安定モデルに基づいた命題レベルの極小更新仕様計算を提案した.
以上の背景を踏まえ,今年度の目的を,以下の2点に設定した.
・平成9年度の結果を拡張し,一階述語レベルの極小更新仕様計算の理論的基礎を与え,仮説論理プログラムへの変更を用いることによって実装する.
・演繹データベースの更新などに応用して妥当性を検証する.
平成10年度の成果は以下である.
・関数記号なしの一階述語レベルの極小更新仕様計算に関して一般化安定モデルと極小更新仕様の関係を明らかにし,さらにその手続きが以前提案した一般化安定モデルに対するトップダウンの証明手続きの援用によって実装できることを明らかにした.
・ソフトウェア工学でのBorgidaの極小更新仕様およびBalzerのPollution Markerの実装を上記の方法で行い,妥当性を検証した.