文献

J-GLOBAL ID：201902270161955649   整理番号：19A1136691

幾何学のためのポートフォリオ定理証明と証明器の予測【JST・京大機械翻訳】

Portfolio theorem proving and prover runtime prediction for geometry

著者 (4件)： Nikolic Mladen (Faculty of Mathematics, University of Belgrade, Belgrade, Serbia) ,  Marinkovic Vesna (Faculty of Mathematics, University of Belgrade, Belgrade, Serbia) ,  Kovacs Zoltan (The Priv. Univ. College of Educ. of the Diocese of Linz, Linz, Austria) ,  Janicic Predrag (Faculty of Mathematics, University of Belgrade, Belgrade, Serbia)
資料名： Annals of Mathematics and Artificial Intelligence  (Annals of Mathematics and Artificial Intelligence)
巻： 85  号： 2-4  ページ： 119-146  発行年： 2019年 
JST資料番号： W2049A  ISSN： 1012-2443  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 近年,ポートフォリオ問題解決は自動推論において多くの応用を見出し,主にSAT解法と自動化および相互作用定理証明においてある。ポートフォリオ問題解決は,特定の問題の個々のインスタンスに対するアプローチであり,特に,最も適切で,解決技術は,いくつかの利用可能なものの中で自動的に選択され,使用される。選択は通常機械学習法を採用する。著者らの知識に対して,このアプローチは,これまでの幾何学で証明された自動化定理では使用されておらず,多くの新しい課題を提起している。本論文では,機械学習技術が幾何学的に使用できるように,特定の幾何学的定理を特徴付ける特徴集合を提案した。これらの特徴に依存し,異なる機械学習技術を用いて,幾何学における定理証明のためのいくつかのポートフォリオを構築し,また,含まれるプローブに対する実行時間予測モデルも構築した。幾何学的定理の二つのコーパスについて評価を行った。一つは幾何学的構成問題から,もう一つはGeoGebraツールのベンチマーク集合からのものである。得られた結果は,機械学習技術が幾何学における自動化定理証明において有用であることを示し,一方,更なる進歩の余地がある。Copyright 2018 Springer Nature Switzerland AG Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 自動化 ,  *ポートフォリオ ,  ベンチマーク ,  *定理証明 ,  問題解決 ,  機械学習 ,  相互作用 ,  *幾何学 ,  アルゴリズム ,  コーパス ,  プローブ ,  *予測 ,  予測モデル
準シソーラス用語： 機械学習技術 ,  自動推論 , 【Automatic Indexing@JST】

著者キーワード (3件)： アルゴリズム的ポータル ,  実行予測 ,  幾何学における自動定理証明

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

タイトルに関連する用語 (5件)： 幾何学 ,  ポートフォリオ ,  定理証明 ,  証明 ,  予測