モデル生成型定理証明系のAND並列化方式

越村 三幸  長谷川 隆三  

誌名
電子情報通信学会論文誌 D   Vol.J78-D1   No.2   pp.228-238
発行日: 1995/02/25
Online ISSN: 
DOI: 
Print ISSN: 0915-1915
論文種別: 特集論文 (超並列コンピュータシステム論文特集)
専門分野: 応用
キーワード: 
自動証明,  モデル生成,  連言照合,  包摂テスト,  AND並列,  

本文: PDF(762.4KB)
>>論文を購入


あらまし: 
1階述語論理の定理証明系MGTP(Model Generation Theorem Prover)のANDの並列化方式を提案しその評価を行う.MGTPはモデル生成法を証明手法として採用しており,並列記号処理言語KL1で記述されている.モデル生成法における定理証明過程では,一般に場合分けによる分岐を含み,分岐による並列性(OR並列性)を内在しているが,本論文では,このような分岐が全くない場合の並列性(AND並列性)抽出を扱う.本方式では,モデル生成法をgenerate-and-test型の計算としてモデル化し,そこに要求駆動の制御を導入して,並列環境下での負荷の均衡を図っている.方式評価は,分離の規則に関する問題を例に,256台のプロセッサからなる分散メモリ型並列マシンPIM/m上で行い,200倍以上の台数効果を得た.