文献

J-GLOBAL ID：202302225474682482   整理番号：23A0532472

AgdaによるZornの補題の証明

著者 (1件)： 河野真治 (琉球大 工)
資料名： 情報処理学会プログラミング・シンポジウム予稿集  (プログラミング・シンポジウム予稿集)
巻： 64th  ページ： 5-16  発行年： 2023年01月31日 
JST資料番号： G0897A  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 集合論は数学では古典的な基礎なので避けて通れない。AgdaはCurry Howward対応で証明を記述できる純関数型言語である。Agda向きの集合論の公理を提案し,その有用性示すの例題としてZornの補題の証明を行った。Zornの補題はチコノフの定理などに使われる重要な定理であり,それを証明付きデータ構造を用いてAgdaで証明する。直観主義論理での集合論について考察する。(著者抄録)

シソーラス用語： *集合論 ,  *関数型言語 ,  定理証明 ,  データ構造 ,  記号論理 ,  公理 ,  直観論理

分類 (2件)： 計算理論  (JB02000A) ,  汎用プログラミング言語  (JD03051H)

引用文献 (9件)：

• Kurt Gödel. Remarks before the princeton bicentennial conference on problems in mathematics. In Solomon Feferman, John Dawson, and Stephen Kleene, editors, Kurt Gödel: Collected Works Vol. Ii, pages 150-153. Oxford University Press, 1946.
• Jose Grimm. Implementation of bourbaki's elements of mathematics in coq: Part one, theory of sets. Journal of Formalized Reasoning, 3(1):79-126, 2010.
• Shinji Kono. https://github.com/shinji-kono/zf-inagda, 2019.
• Kenneth Kunen. Set theory - an introduction to independence proofs. page 1 - 325, Nov 2008.
• Ulf Norell. Dependently typed programming in agda. In Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI '09, pages 1-2, New York, NY, USA, 2009. ACM.

タイトルに関連する用語 (2件)： 補題 ,  証明