ログイン
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

{"_buckets": {"deposit": "cea9350b-e7a9-497f-9586-faa82efdf35f"}, "_deposit": {"created_by": 3, "id": "145", "owners": [3], "pid": {"revision_id": 0, "type": "depid", "value": "145"}, "status": "published"}, "_oai": {"id": "oai:metro-cit.repo.nii.ac.jp:00000145", "sets": ["21"]}, "author_link": ["658", "657", "998"], "item_1_biblio_info_14": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2013-03", "bibliographicIssueDateType": "Issued"}, "bibliographicPageEnd": "40", "bibliographicPageStart": "26", "bibliographicVolumeNumber": "7", "bibliographic_titles": [{"bibliographic_title": "東京都立産業技術高等専門学校研究紀要"}, {"bibliographic_title": "Research reports of Tokyo Metropolitan College of Industrial Technology", "bibliographic_titleLang": "en"}]}]}, "item_1_creator_6": {"attribute_name": "著者名(日)", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "中西 , 泰雄"}, {"creatorName": "ナカニシ, ヤスオ", "creatorNameLang": "ja-Kana"}], "nameIdentifiers": [{"nameIdentifier": "657", "nameIdentifierScheme": "WEKO"}]}]}, "item_1_creator_7": {"attribute_name": "著者名よみ", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "ナカニシ, ヤスオ"}], "nameIdentifiers": [{"nameIdentifier": "998", "nameIdentifierScheme": "WEKO"}]}]}, "item_1_creator_8": {"attribute_name": "著者名(英)", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Nakanishi, Yasuo", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "658", "nameIdentifierScheme": "WEKO"}]}]}, "item_1_description_1": {"attribute_name": "ページ属性", "attribute_value_mlt": [{"subitem_description": "P(論文)", "subitem_description_type": "Other"}]}, "item_1_description_12": {"attribute_name": "抄録(英)", "attribute_value_mlt": [{"subitem_description": "In a heuristic process of proof in mathematics, we try not only forward derivationsfrom the assumptions such as `from A, we get B\u0027 but also backward derivations from theconclusion such as `in order to get C, we need D\u0027. Thus, we have to discover all the statementswhich connect assumptions with the conclusion, to complete the planning of the proof. Wedefine `heuristic tableau\u0027 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.", "subitem_description_type": "Other"}]}, "item_1_source_id_13": {"attribute_name": "雑誌書誌ID", "attribute_value_mlt": [{"subitem_source_identifier": "AA12210629", "subitem_source_identifier_type": "NCID"}]}, "item_1_text_9": {"attribute_name": "著者所属(日)", "attribute_value_mlt": [{"subitem_text_value": "東京都立産業技術高等専門学校 ものづくり工学科"}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2013-03-01"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "KJ00008928039.pdf", "filesize": [{"value": "95.7 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_11", "mimetype": "application/pdf", "size": 95700.0, "url": {"label": "KJ00008928039", "url": "https://metro-cit.repo.nii.ac.jp/record/145/files/KJ00008928039.pdf"}, "version_id": "d998d6e5-7f29-4bc7-a6cd-1a2a30375408"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "Proo", "subitem_subject_language": "en", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Heuristic Tableau", "subitem_subject_language": "en", "subitem_subject_scheme": "Other"}, {"subitem_subject": "NK", "subitem_subject_language": "en", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "departmental bulletin paper", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "発見タブローによる証明計画", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "発見タブローによる証明計画"}, {"subitem_title": "Planning of Proof by Heuristic Tableau", "subitem_title_language": "en"}]}, "item_type_id": "1", "owner": "3", "path": ["21"], "permalink_uri": "https://metro-cit.repo.nii.ac.jp/records/145", "pubdate": {"attribute_name": "公開日", "attribute_value": "2013-03-01"}, "publish_date": "2013-03-01", "publish_status": "0", "recid": "145", "relation": {}, "relation_version_is_last": true, "title": ["発見タブローによる証明計画"], "weko_shared_id": 3}
  1. 紀要
  2. 東京都立産業技術高等専門学校研究紀要
  3. 7

発見タブローによる証明計画

https://metro-cit.repo.nii.ac.jp/records/145
https://metro-cit.repo.nii.ac.jp/records/145
813cb098-90d7-4820-9e07-82fd5d2d0ba6
名前 / ファイル ライセンス アクション
KJ00008928039.pdf KJ00008928039 (95.7 kB)
license.icon
Item type 紀要論文(ELS) / Departmental Bulletin Paper(1)
公開日 2013-03-01
タイトル
タイトル 発見タブローによる証明計画
タイトル
言語 en
タイトル Planning of Proof by Heuristic Tableau
言語
言語 jpn
キーワード
言語 en
主題 Proo
キーワード
言語 en
主題 Heuristic Tableau
キーワード
言語 en
主題 NK
資源タイプ
資源タイプ識別子 http://purl.org/coar/resource_type/c_6501
資源タイプ departmental bulletin paper
ページ属性
内容記述タイプ Other
内容記述 P(論文)
著者名(日) 中西 , 泰雄

× 中西 , 泰雄

WEKO 657

中西 , 泰雄

ja-Kana ナカニシ, ヤスオ

Search repository
著者名よみ ナカニシ, ヤスオ

× ナカニシ, ヤスオ

WEKO 998

ナカニシ, ヤスオ

Search repository
著者名(英) Nakanishi, Yasuo

× Nakanishi, Yasuo

WEKO 658

en Nakanishi, Yasuo

Search repository
著者所属(日)
東京都立産業技術高等専門学校 ものづくり工学科
抄録(英)
内容記述タイプ 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.
雑誌書誌ID
収録物識別子タイプ NCID
収録物識別子 AA12210629
書誌情報 東京都立産業技術高等専門学校研究紀要
en : Research reports of Tokyo Metropolitan College of Industrial Technology

巻 7, p. 26-40, 発行日 2013-03
戻る
0
views
See details
Views

Versions

Ver.1 2023-05-15 11:22:39.800435
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3