文献

J-GLOBAL ID：201802245201591824   整理番号：18A2003938

AGDAにおける構成的射影幾何学の形式化【JST・京大機械翻訳】

Formalizing Constructive Projective Geometry in Agda

著者 (1件)： Calderon Guillermo (University of the Republic, Montevideo, Uruguay)
資料名： Electronic Notes in Theoretical Computer Science  (Electronic Notes in Theoretical Computer Science)
巻： 338  ページ： 61-77  発行年： 2018年 
JST資料番号： W2857A  ISSN： 1571-0661  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： 証明支援とプログラミング言語Agdaにおける射影幾何学の形式化を提示した。著者らは,構築的に有効な方法だけを適用する領域において,ほとんどの伝統的な話題をカバーするために適切であることを示した建設的射影幾何学における最近の発展を定式化した。射影幾何学のための他のよく知られた構成的公理システムとの等価性を証明し,定式化した。この実装は,公理,双対性の原理,FanoとDesasesの特性および調和共役を含む直観的合成射影平面幾何学の基本的なフラグメントをカバーする。著者らは,文献において部分的かつあいまいに記述される複雑で大規模な証明の実施例に焦点を当てた。すなわち,調和共役の一意性である。著者らの実装の最も重要な詳細を記述し,モジュール,依存記録タイプ,暗黙の議論,および形式的証明の典型的な正当性を減少させるために非常に役に立つ事例のようなAgdaのいくつかの興味深い特性を利用する方法を示した。Copyright 2018 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： *射影 ,  等価性 ,  プログラミング言語 ,  曖昧さ ,  公理 ,  双対性 ,  一意性 ,  共役 ,  *幾何学 ,  定式化 ,  *射影幾何学
準シソーラス用語： 適用事例 , 【Automatic Indexing@JST】

著者キーワード (5件)： アシスタントの証明 ,  数学の形式化 ,  射影幾何学 ,  型理論 ,  AGDA

分類 (1件)： 図形・画像処理一般  (JE04010I)

タイトルに関連する用語 (2件)： 射影幾何学 ,  形式化