自動定理証明における補助命題の実装について ―幾何学基礎論を題材として―

• 資料種別: 博士論文
• タイトル: 自動定理証明における補助命題の実装について ―幾何学基礎論を題材として―
• 著者・編者: 岩間, 詞也; Fumiya, IWAMA
• 著者標目: 岩間, 詞也; Fumiya, IWAMA
• 出版年月日等: 2023-03-31
• 出版年（W3CDTF）: 2023-03-31
• 並列タイトル等: Implementation of Sublemma in Automated Theorem Proving. ―Subject to Foundation of Geometry―
• 授与機関名: 甲南大学
• 授与年月日: 2023-03-31
• 授与年月日（W3CDTF）: 2023-03-31
• 報告番号: 甲第126号
• 学位: 博士（工学）
• 本文の言語コード: jpn
• 件名標目: 自動定理証明; 幾何学基礎論; Automated Theorem Proving; Foundation Geometry
• 対象利用者: 一般
• 一般注記: 自動定理証明（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年度)
• DOI: 10.14990/00004570; https://doi.org/10.14990/00004570
• 国立国会図書館永続的識別子: info:ndljp/pid/12864251; https://dl.ndl.go.jp/pid/12864251
• コレクション（共通）: 障害者向け資料
• コレクション（障害者向け資料：レベル1）: テキストデータ
• コレクション（個別）: 国立国会図書館デジタルコレクション > デジタル化資料 > 博士論文; https://dl.ndl.go.jp/collections/A00014
• 収集根拠: 博士論文（自動収集）
• 受理日（W3CDTF）: 2023-05-05T22:12:36+09:00
• 記録形式（IMT）: application/pdf
• オンライン閲覧公開範囲: 国立国会図書館内限定公開
• デジタル化資料送信: 図書館・個人送信対象外
• 遠隔複写可否（NDL）: 可
• 掲載誌（URI）: http://dx.doi.org/10.14990/00004570; http://id.nii.ac.jp/1260/00004570/
• 連携機関・データベース: 国立国会図書館 : 国立国会図書館デジタルコレクション; https://dl.ndl.go.jp