文献

J-GLOBAL ID：201902268787428681   整理番号：19A0981955

並列事後および連続性公理:Coqを用いた直感論理における機械化研究【JST・京大機械翻訳】

Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq

著者 (4件)： Boutry Pierre (ICube, UMR 7357 CNRS, University of Strasbourg, Illkirch, France) ,  Gries Charly (ICube, UMR 7357 CNRS, University of Strasbourg, Illkirch, France) ,  Narboux Julien (ICube, UMR 7357 CNRS, University of Strasbourg, Illkirch, France) ,  Schreck Pascal (ICube, UMR 7357 CNRS, University of Strasbourg, Illkirch, France)
資料名： Journal of Automated Reasoning  (Journal of Automated Reasoning)
巻： 62  号： 1  ページ： 1-68  発行年： 2019年 
JST資料番号： D0269E  ISSN： 0168-7433  CODEN： JAREEW  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 本論文において,著者らは,Euclidの5番目の仮説の異なるバージョンの間の等価性の証明の形式化に焦点を合わせた。著者らの研究は,Tarskiの中立幾何学の文脈において,または,公理の最初の3つのグループによって定義されたHilbertの幾何学において等価的に実行されて,点等式に対して排他的な中間だけを仮定して,直観論理を使用する。著者らの形式化は,ポストレートの異なるバージョンが等価である条件の明確化を提供する。Beesonに従って,ポストレートのバージョンが等価で,構成的であるかどうかを研究した。著者らは,4つのグループの並列推論を区別した。各グループにおいて,それらの等価性を,連続性仮定なしで直観論理を用いて機械化した。グループ間の等価性に対して,追加の仮定が必要である。34個のポストレートの間の等価性は,アルキメデス平面中立幾何学において定式化される。また,Szmielwによる定理の変種を定式化した。この変異状態は,Aristotleの公理を仮定して,ユークリッド面に保持されている任意のステートメントが,Euclidの5番目の仮説に等価であることを示している。すべてのこれらの結果を得るために,角度の和の概念の形式化と,Archimedesの公理を仮定しているSaceri-Legendre定理の証明を含む平面中立幾何学における大きなライブラリーを開発した。三角形における角度の和は,ほとんど2つの直角である。Copyright 2017 Springer Science+Business Media B.V. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 幾何学 ,  等価性 ,  *連続性 ,  変異 ,  定式化 ,  *公理 ,  *機械化

著者キーワード (12件)： Euclid ,  並列郵便物 ,  形式化 ,  中性幾何学 ,  Coq ,  分類 ,  幾何学の基礎 ,  交差点の決定可能性 ,  アリストトルの公理 ,  アルキメデスの公理 ,  Sacceri-Legendre定理 ,  角の和

分類 (1件)： 計算理論  (JB02000A)

タイトルに関連する用語 (6件)： 連続性 ,  公理 ,  直感 ,  論理 ,  機械化 ,  研究