複数の簡約順序のもとでの項書換えシステム完備化手続き

近藤 久  栗原 正仁  大内 東  

誌名
電子情報通信学会論文誌 D   Vol.J78-D1    No.1    pp.1-10
発行日: 1995/01/25
Online ISSN: 
DOI: 
Print ISSN: 0915-1915
論文種別: 論文
専門分野: ソフトウェア基礎
キーワード: 
Knuth-Bendix完備化手続き,  停止性,  合流性,  項書換えシステム,  ATMS(Assumption-based TMS),  

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



あらまし: 
Knuth-Bendix完備化手続きは,簡約順序と等式集合が与えられたとき,(1)完備な項書換えシステムを生成し成功する,(2)ある等式をその簡約順序で向き付けられずに失敗する,(3)無限に手続きが停止せずに発散する,のいずれかの結果を生ずる.完備化の成功は与えられた簡約順序に大きく依存する.本論文では,利用者の簡約順序の決定の負担を軽減し,不適当な簡約順序による手続きの発散を避けるため,複数の簡約順序を扱う完備化手続きを提案する.本手法は効率化のため,人工知能の分野で提案されているアーキテクチャであるATMSのデータ構造に基づいたノードと呼ばれるデータを用い,各簡約順序のもとで通常の完備化を並行に実行することをシミュレートする.その際,ATMSの多重文脈を扱う性質を用い,推論結果を各簡約順序間で共有することによって重複した推論を避ける.