WEKO3
-
RootNode
アイテム
定理証明システムSENRIの構成
https://ipsj.ixsq.nii.ac.jp/records/15983
https://ipsj.ixsq.nii.ac.jp/records/1598383f821be-019d-45a0-b336-96d20f952000
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-JNL2501006.pdf (843.3 kB)
|
Copyright (c) 1984 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Journal(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 1984-01-15 | |||||||
| タイトル | ||||||||
| タイトル | 定理証明システムSENRIの構成 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | The Organization of Theorem Proving System "SENRI" | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 大阪大学工学部通信工学科 | ||||||||
| 著者所属 | ||||||||
| 山口大学情報処理センター | ||||||||
| 著者所属 | ||||||||
| 大阪大学工学部通信工学科 | ||||||||
| 著者所属 | ||||||||
| 大阪大学工学部通信工学科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Faculty of Engineering, Osaka University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Information Processing Center, Yamaguchi University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Faculty of Engineering, Osaka University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Faculty of Engineering, Osaka University | ||||||||
| 著者名 |
山口, 高平
西岡, 弘明
打浪, 清一
手塚慶一
× 山口, 高平 西岡, 弘明 打浪, 清一 手塚慶一
|
|||||||
| 著者名(英) |
Takahira, Yamaguchi
Hiroaki, Nishioka
Seiichi, Uchinami
Yoshikazu, Tezuka
× Takahira, Yamaguchi Hiroaki, Nishioka Seiichi, Uchinami Yoshikazu, Tezuka
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 従来の定理証明システムは 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で作成したので 拡張性および移植性が高く 最後に表示は論理学で用いられる表記法に近いものを採用したので 入力が容易で出力が見やすいものになっていることが挙げられる. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN00116647 | |||||||
| 書誌情報 |
情報処理学会論文誌 巻 25, 号 1, p. 46-58, 発行日 1984-01-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7764 | |||||||
