WEKO3
アイテム
発見タブローによる証明計画
https://metro-cit.repo.nii.ac.jp/records/145
https://metro-cit.repo.nii.ac.jp/records/145813cb098-90d7-4820-9e07-82fd5d2d0ba6
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
KJ00008928039 (95.7 kB)
|
.png)
|
| Item type | 紀要論文(ELS) / Departmental Bulletin Paper(1) | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2013-03-01 | |||||||||||||
| タイトル | ||||||||||||||
| タイトル | 発見タブローによる証明計画 | |||||||||||||
| 言語 | ja | |||||||||||||
| タイトル | ||||||||||||||
| タイトル | Planning of Proof by Heuristic Tableau | |||||||||||||
| 言語 | en | |||||||||||||
| 言語 | ||||||||||||||
| 言語 | jpn | |||||||||||||
| キーワード | ||||||||||||||
| 言語 | en | |||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | Proo | |||||||||||||
| キーワード | ||||||||||||||
| 言語 | en | |||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | Heuristic Tableau | |||||||||||||
| キーワード | ||||||||||||||
| 言語 | en | |||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | NK | |||||||||||||
| 資源タイプ | ||||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||||||
| 資源タイプ | departmental bulletin paper | |||||||||||||
| ページ属性 | ||||||||||||||
| 内容記述タイプ | Other | |||||||||||||
| 内容記述 | P(論文) | |||||||||||||
| 言語 | ja | |||||||||||||
| 著者名(日) |
中西, 泰雄
× 中西, 泰雄
|
|||||||||||||
| 著者所属(日) | ||||||||||||||
| ja | ||||||||||||||
| 東京都立産業技術高等専門学校 ものづくり工学科 | ||||||||||||||
| 抄録(英) | ||||||||||||||
| 内容記述タイプ | Other | |||||||||||||
| 内容記述 | In a heuristic process of proof in mathematics, we try not only forward derivationsfrom the assumptions such as `from A, we get B' but also backward derivations from theconclusion such as `in order to get C, we need D'. Thus, we have to discover all the statementswhich connect assumptions with the conclusion, to complete the planning of the proof. Wedefine `heuristic tableau' as a tableau which consists of those statements aranged in the order of discovery with symbols which express the logical relations of those statements. We suggesta planning method of proofs by using heuristic tableaus. For a concrete explanation, we use the first order NK system of Gentzen to explain our method. Our method gives an algorithmto prove arbitrary tautologies of the first order NK system, and is also valid for practical mathematics which is not necessarily formalized in symbolic logic. | |||||||||||||
| 言語 | en | |||||||||||||
| 書誌情報 |
ja : 東京都立産業技術高等専門学校研究紀要 en : Research reports of Tokyo Metropolitan College of Industrial Technology 巻 7, p. 26-40, 発行日 2013-03 |
|||||||||||||
| 出版者 | ||||||||||||||
| 出版者 | 東京都立産業技術高等専門学校 | |||||||||||||
| 言語 | ja | |||||||||||||
| ISSN | ||||||||||||||
| 収録物識別子タイプ | PISSN | |||||||||||||
| 収録物識別子 | 18831990 | |||||||||||||
| 書誌レコードID | ||||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||||
| 収録物識別子 | AA12210629 | |||||||||||||
