@article{oai:ipsj.ixsq.nii.ac.jp:00015983,
 author = {山口, 高平 and 西岡, 弘明 and 打浪, 清一 and 手塚慶一 and Takahira, Yamaguchi and Hiroaki, Nishioka and Seiichi, Uchinami and Yoshikazu, Tezuka},
 issue = {1},
 journal = {情報処理学会論文誌},
 month = {Jan},
 note = {従来の定理証明システムは LISPで一つの定理証明法を構成することに重点が置かれていたが 使いやすさや効率面で問題があった.そこで本稿では オプションの指定を変更するだけで さまざまな定理証明法を構成でき また反駁が得られない場合 支援システムが稼動し 適切な戦略を再設定できるように助言を与えることを新しい特徴とする定理証明システムSENRI(System to Evaluate Non-numeRical Informations)を構築した.次にLISPでシステムを構築すると 記憶領域の管理は廃品回収(GC)を使用せざるをえないが SENRIでは 将来必要となる記憶領域は節集合領域だけであることに着目し LAVS(List of AVailable Space)を節集合領域と一時作業領域に2分割し 両方向から使用してあふれが生じたとき 一時作業領域のポインタを再設定するだけでLAVSを再利用するという新しい記憶領域の管理法を提案し GCと比較してLAVSの再構成時間が極度に短縮されることを確認した.またSENRIのリスト構造は 2進木リストに比べて 述語論理式をコンパクトに表現している.その他 SENRI の特徴としては 頻繁に使用されるルーチンのアセンブラ・バージョンを作成することにより1回当りの導出時間を短縮しており また元バージョンはモジュール別にFORTRANで作成したので 拡張性および移植性が高く 最後に表示は論理学で用いられる表記法に近いものを採用したので 入力が容易で出力が見やすいものになっていることが挙げられる.},
 pages = {46--58},
 title = {定理証明システムSENRIの構成},
 volume = {25},
 year = {1984}
}