WEKO3
アイテム
Agda 上でのZF集合論の構成
https://ipsj.ixsq.nii.ac.jp/records/232259
https://ipsj.ixsq.nii.ac.jp/records/232259bbdc3507-3e89-42b0-8dcc-f9ba17ec2caf
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WPRO2020006.pdf (999.2 kB)
|
Copyright (c) 2020 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2020-01-10 | |||||||
| タイトル | ||||||||
| タイトル | Agda 上でのZF集合論の構成 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Constructing a model of ZF Set Theory on Agda | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | Agda, Set-Theory, Proof | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
| 資源タイプ | conference paper | |||||||
| 著者所属 | ||||||||
| 琉球大学工学部 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Faculty of Engineering, University of the Ryukyus | ||||||||
| 著者名 |
河野, 真治
× 河野, 真治
|
|||||||
| 著者名(英) |
Shinji, Kono
× Shinji, Kono
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | Agda は省略可能な型変数を持つ純関数型言語であり、カーリーハワード対応に基づく証明支援系として使うことができる。数学的な命題は型として記述され、その証明は型を実現するλ項としてされる。ここでは直観主義論理に適した非構成的な仮定を導入し、ZFC集合論の公理を証明する。集合はデータ構造である順序数上の述語(Ordinal definable)として導入する。 | |||||||
| 書誌情報 |
第61回プログラミング・シンポジウム予稿集 巻 2020, p. 23-34, 発行日 2020-01-10 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
