述語論理的プログラムの理論及び実装

1990 年度 実績報告書

• 研究課題/領域番号: 02452153
• 研究機関: 筑波大学
• 研究代表者: 五十嵐 滋 筑波大学, 電子・情報工学系, 教授 (80027367)
• 研究分担者: 水谷 哲也 埼玉短期大学, 情報処理学科, 助教授 (70209758) ; 大木 敦雄 筑波大学, 社会工学系, 助手 (20160434) ; 細野 千春 筑波大学, 電子・情報工学系, 講師 (20108294) ; 辻 尚史 筑波大学, 電子・情報工学系, 助教授 (70016666)
• キーワード: Uー転換 / NU / 軌跡準同型 / 人工知能 / 同値理論 / 不完全情報ゲ-ム / 音楽情報処理

研究概要

各研究分担者は、解析的意味論に基づく述語論理的プログラム言語NUの理論の構築及び処理系の作成を行なった。NUは、論理的プログラム言語であるうえに手続き的な表現ができ、さらにプログラムの要求仕様と相互に変換が容易であるという特徴をもつ。主な研究業績は、以下の3項目である。
1 NUの理論面の研究として、以下の4点について一定の成果が得られ、それらを公表した。
(1)NUで表現された並行プログムに関する同値理論(軌跡準同型写像)の基礎的研究およびその応用を行った。
(2)疎結合でかつデ-タ信号や制御信号が一方向にしか送られないような2つのプロセスの間で実際に発生した具体的な実時間問題について、解析、検証を行った。
(3)並行プログラムをNUで表現する新たな方法を開発し、その上で検証システムついて研究した。
(4)プログラムのリファインメントおよび同値性を自動的に判定するシステムについて研究した。
2 不完全情報ゲ-ムや音楽情報処理という、高度に知的な人工知能的課題について、以下の2点を公表した。
(1)不完全情報ゲ-ムであるコントラクトブリッジの終盤のプレイについて、必勝形であるか否かを論理的に表現し、それを手続き型プログラムに翻訳、実行した。
(2)音楽情報処理について、演奏家の特徴を定量的に抽出し、それらを解析した。
3 NU処理系については、高速化を計るとともに、高階述語論理に基づく部分を自由に取り扱えるようにするなど、拡張された構文に対する処理が行なえるようにした。また、パズルやCADなどの問題のNUによる論理的表現についても研究した。これらの研究成果のうち一部は公表した。

研究成果

• [文献書誌] Tetsuya Mizutani,Shigeru Igarashi,Takashi Tsuji: "An analytical equivalence theory of computer programs" International symposium on structures in mathematical theories. 199-204 (1990)
• [文献書誌] 北島 伸克,池田 靖雄,細野 千春,五十嵐 滋: "vー行為における並行プログラム系のスケジュ-リング" 日本ソフトウェア科学会第7回(1990)大会論文集. 141-144 (1990)
• [文献書誌] 富田 康治,辻 尚史,五十嵐 滋: "プログラムにおける実時間問題" 日本ソフトウェア科学会第7回(1990)大会論文集. 153-156 (1990)
• [文献書誌] 水谷 哲也,辻 尚史,五十嵐 滋: "並行プログラム系の軌跡準同型" 日本ソフトウェア科学会第7回(1990)大会論文集. 157-160 (1990)
• [文献書誌] 池田 靖雄,細野 千春,辻 尚史,五十嵐 滋: "NU解釈系の設計" 日本ソフトウェア科学会第7回(1990)大会論文集. 293-296 (1990)
• [文献書誌] 池田 信之,五十嵐 滋,水谷 哲也,細野 千春,辻 尚史: "プログラムのリファインメントと同値性について" 応用数学合同研究集会報告集. 80-85 (1990)
• [文献書誌] 池田 靖雄,細野 千春,辻 尚史,五十嵐 滋: "閉じた論理式の証明系としてのν行為解釈系の設計" 応用数学合同研究集会報告集. 88-93 (1990)
• [文献書誌] 池田 靖雄,細野 千春,辻 尚史,五十嵐 滋: "論理式言語NUおける知的プログラム" 第32回プログラミングシンポジウム報告集. 39-50 (1991)
• [文献書誌] 市中 康公,五十嵐 滋: "音楽情報処理としてのピアノ演奏の特徴抽出" 情報処理学会第42回(平成3年前期)全国大会講演論文集. (1991)
• [文献書誌] 佐々木 裕,細野 千春,辻 尚史,五十嵐 滋: "ブリッジプレイの終盤における必勝戦術の論理的孝察" 情報処理学会第42回(平成3年前期)全国大会講演論文集. (1991)