このブラウザは、JavaScript が無効になっています。JavaScriptを有効にして再度、お越しください。
ログイン
甲南大学機関リポジトリとは
本大学において生産された電子的な学術研究成果物及び教育成果物を蓄積・保存し、インターネットを使って学内外に無償で公開することにより、学術研究及び教育の発展並びに社会に対する貢献を果たすことを目的としています。
甲南大学機関リポジトリ
トップ
ランキング
詳細検索
全文検索
キーワード検索
タイトル
著者名 OR 著者ID
キーワード
抄録・内容記述
公開者 OR 著者ID
寄与者 OR 著者ID
資源タイプ
雑誌名
出版年
学位授与番号
インデックス
WEKO著者ID
AND
タイトル
著者名 OR 著者ID
キーワード
抄録・内容記述
公開者 OR 著者ID
寄与者 OR 著者ID
資源タイプ
雑誌名
出版年
学位授与番号
インデックス
WEKO著者ID
AND
タイトル
著者名 OR 著者ID
キーワード
抄録・内容記述
公開者 OR 著者ID
寄与者 OR 著者ID
資源タイプ
雑誌名
出版年
学位授与番号
インデックス
WEKO著者ID
AND
タイトル
著者名 OR 著者ID
キーワード
抄録・内容記述
公開者 OR 著者ID
寄与者 OR 著者ID
資源タイプ
雑誌名
出版年
学位授与番号
インデックス
WEKO著者ID
AND
タイトル
著者名 OR 著者ID
キーワード
抄録・内容記述
公開者 OR 著者ID
寄与者 OR 著者ID
資源タイプ
雑誌名
出版年
学位授与番号
インデックス
WEKO著者ID
AND
タイトル
著者名 OR 著者ID
キーワード
抄録・内容記述
公開者 OR 著者ID
寄与者 OR 著者ID
資源タイプ
雑誌名
出版年
学位授与番号
インデックス
WEKO著者ID
検索条件を追加
検索条件を追加
NIIsubject
NDC
NDLC
BSH
NDLSH
MeSH
DDC
LCC
UDC
LCSH
紀要論文(ELS) / Departmental Bulletin Paper
紀要論文 / Departmental Bulletin Paper_02
学術雑誌論文 / Journal Article
紀要論文 / Departmental Bulletin Paper
会議発表論文 / Conference Paper
一般雑誌記事 / Article
会議発表用資料 / Presentation
学位論文 / Thesis or Dissertation
報告書 / Research Paper
図書 / Book
図書の一部 / Book
その他 / Others
DublinCore
Journal Article
Thesis or Dissertation
Departmental Bulletin Paper
Conference Paper
Presentation
Book
Technical Report
Research Paper
Article
Preprint
Learning Material
Data or Dataset
Software
Others
Learning Object Metadata
LIDO
Journal Article
Thesis or Dissertation
Departmental Bulletin Paper
Conference Paper
Presentation
Book
Technical Report
Research Paper
Article
Preprint
Learning Material
Data or Dataset
Software
Others
identifier
URI
fullTextURL
selfDOI
ISBN
ISSN
NCID
pmid
doi
NAID
ichushi
日本語
英語
フランス語
イタリア語
ドイツ語
スペイン語
中国語
ロシア語
ラテン語
マレー語
エスペラント語
アラビア語
ギリシャ語
朝鮮語
その他の言語
CC BY
CC BY-SA
CC BY-ND
CC BY-NC
CC BY-NC-SA
CC BY-NC-ND
自由記述
author
publisher
ETD
none
Language
日本語
English
インデックスツリー
インデックス
博士論文
令和4年度 (2022年度)
Permalink : http://doi.org/10.14990/00004570
自動定理証明における補助命題の実装について ―幾何学基礎論を題材として―
利用統計を見る
File / Name
License
本文
本文 (1.17MB)
[ 28 downloads ]
論文内容の要旨及び論文審査の結果の要旨
論文内容の要旨及び論文審査の結果の要旨 (357.71KB)
[ 16 downloads ]
JaLC DOI
info:doi/10.14990/00004570
アイテムタイプ
学位論文 / Thesis or Dissertation
言語
日本語
キーワード
自動定理証明, 幾何学基礎論
著者
岩間 詞也
/ イワマ フミヤ
抄録
自動定理証明（Automated theorem proving, ATP）は，自動推論 (AR) の中でも最も成功している研究分野であり，コンピュータプログラム（ソフトウェア）によって数学的定理に対する証明を発見することを目的としている。ATPを用いて数学の定理証明を実行するには，ソフトウェアが認識可能な形で理論に沿った条件を構築しなければならない。これまで人間がATPを用いずに行ってきた証明と，ATPを用いた証明には差異が存在し，それを解消するための技法は研究の途上にある。ATPを活用するには，数学的対象と関係の構築を表現する手順と関連する概念についての洞察が必要である。ATPが人間の証明を支援することで証明の精度を高めることができる。そこに定理証明にATPを用いる価値がある。
ユークリッド幾何学は，点・線・面などの定義および一連の公理・公準が与えられ，それらを基に理論体系が構築されている。それに対し，ヒルベルトはユークリッド幾何学の点・線・面などの定義が数学的に厳密ではないとして，公理のなかでそれらの関係性のみを構築することで厳密化を図った。ATPは，こうした数学的定理の妥当性・整合性を機械的に確認する目的で開発されたものである。ヒルベルトによる幾何学基礎論の証明（ユークリッド幾何学の定理証明）をATPの１つであるIsabelle/HOLを用いて試みると，そのままでは証明できない定理が多い。この問題を解決するために，本研究ではユークリッド幾何学の定理証明に対し，ヒルベルトの幾何学基礎論の手法を基に，Isabelle/HOLを用いて証明するための補助命題の実装を行なった。
本論文では，第1章において，ATPおよびその成り立ちとATPが扱える各種問題について実装例を交えて示し，第2章において，ATP機能を有するソフトウェア(定理証明支援系)の現状と補助命題の必要性を明らかにした。そして第3章では，題材としてヒルベルトの幾何学基礎論の証明を基に，ユークリッド幾何学の定理をIsabelle/HOLを用いて証明するために必要な補助命題の実装を行い，その過程において生じる問題およびその解決について明らかにし，最後に第4章において，現状では高階述語論理は決定不能であるが，Isabelle/HOL を用いて人間の証明を支援することで証明の精度を高めることができ，そこに Isabelle/HOL を用いた自動定理証明の価値があることを考察し，今後の課題および発展可能性を示した。
学位名
博士（工学）
学位授与機関
甲南大学
学位授与年度
令和4年度(2022年度)
学位授与年月日
2023-03-31
学位授与番号
34506甲第126号
フォーマット
application/pdf
著者版フラグ
ETD
甲南大学 〒658-8501 神戸市東灘区岡本8丁目9番1号
Konan University 8-9-1, Okamoto, Higashinadaku, Kobe, Japan.
メニュー
トップページ
甲南大学機関リポジトリ規程
登録申請について
登録申請書式
（１）登録申請書
◆
個別申請用【様式1】
（記入例）
◆
発行物単位申請用【様式2】
（記入例）
（２）同意書
＊必要な場合のみ
◆
個別申請用同意書（例）
（記入例）
◆
発行物単位申請用同意書（例）
（記入例）
＞
詳細
Ｑ＆Ａ集
検索
著作権と機関リポジトリＱ＆Ａ
各論文のＵＲＬ（ＤＯＩ）と利用状況確認について
紀要論文の登録について(紀要担当者へのご案内）
リンク
検索
甲南大学
甲南大学図書館
カウンタ
COUNTER
Powered by
WEKO
自動定理証明における補助命題の実装について ―幾何学基礎論を題材として―
本文
(1.17MB)
トップページ
