WEKO3
アイテム
証明の失敗から得られる情報を用いる様相論理定理証明戦略
https://ipsj.ixsq.nii.ac.jp/records/127547
https://ipsj.ixsq.nii.ac.jp/records/1275471f72bf10-9337-4c91-9fed-8343a1d8afb2
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
KJ00001333934.pdf (165.7 kB)
|
|
| Item type | National Convention(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 1995-03-15 | |||||
| タイトル | ||||||
| タイトル | 証明の失敗から得られる情報を用いる様相論理定理証明戦略 | |||||
| タイトル | ||||||
| 言語 | en | |||||
| タイトル | Proof Strategies in Modal Logic Using the Information from the Failure of the Past Proof Process | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||
| 資源タイプ | conference paper | |||||
| 著者所属 | ||||||
| 東京工業大学理工学研究科情報工学専攻 | ||||||
| 著者所属 | ||||||
| 東京工業大学情報理工学研究科計算工学専攻 | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Department of Computer Science, Graduate School of science and engineering, Tokyo Institute of Technology, Japan | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Department of Computer Science, Graduate School of information and engineering, Tokyo Institute or Technology, Japan | ||||||
| 論文抄録 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 自動定理証明に向いた様相論理の一般的証明器に、CCMU^<ss>がある。CCMU^<ss>における証明とは、証明すべき式から得られる様相記号列対をすべて統一化できるように、部分式を複製することである。しかし、不必要な部分式を複製すると証明の効率が著しく低下する。さらに複製した結果得られる式は複製以前の式と類似しており、証明過程で、類似した計算をできる限り行わないようにしたい。そこで、CCMU^<ss>における定理証明戦略として、統一化の失敗情報を用いて、重複する部分式を選択する方法と、複製する前の計算結果を再利用する方法を提案する。これにより、証明しやすい式変形と計算の再利用が可能となり、証明を効率化することができる。 | |||||
| 書誌レコードID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AN00349328 | |||||
| 書誌情報 |
全国大会講演論文集 巻 第50回, 号 人工知能及び認知科学, p. 5-6, 発行日 1995-03-15 |
|||||
| 出版者 | ||||||
| 言語 | ja | |||||
| 出版者 | 情報処理学会 | |||||
