文献

J-GLOBAL ID：202202279117827249   整理番号：22A0496811

新しい一次公式計量に基づく大理論上の公理選択【JST・京大機械翻訳】

Axiom selection over large theory based on new first-order formula metrics

著者 (2件)： Liu Qinghua (School of Information Science and Technology, Southwest Jiaotong University, Chengdu, Sichuan Province, China) ,  Xu Yang (School of Mathematics, Southwest Jiaotong University, Chengdu, Sichuan Province, China)
資料名： Applied Intelligence  (Applied Intelligence)
巻： 52  号： 2  ページ： 1793-1807  発行年： 2022年 
JST資料番号： W0297A  ISSN： 0924-669X  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 公理選択は,与えられた予測を証明するための大規模公理集合から最も可能性のある有用な公理を選択するタスクである。既存の公理選択法は,単に浅い記号を考慮し,相同問題から以前の成功する証明に強く依存している。これらの問題に取り組むために,公式間の非類似性を評価し,選択タスクにおける評価者としてそれを利用するための新しいメトリックを導入した。最初に,項間の非類似性を計算するための置換ベースメトリックを提案した。それは,擬似計量であり,機能的および可変項の両方によって,徹底した構文差を捕えることができる。次に,それを原子に拡張し,原子メトリックも擬似測定であることを証明した。原子集合として公式を処理し,公式間の3種類の非類似性計量を定義した。最後に,著者らは,新しく提案した公式計量に基づく予測指向公理選択法を設計し,実装した。MPTP2078ベンチマーク上で実験評価を行い,非類似性ベースアキシム選択がE証明器の性能を改善することを実証した。最良の場合,それは30.90%から42.25%まで成功する証明の比率を増加させる。Copyright The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature 2021 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： *公理 ,  ベンチマーク

著者キーワード (4件)： 公式計量 ,  公理選択 ,  非類似性 ,  自動定理証明

分類 (2件)： 人工知能  (JE08000Z) ,  計算理論  (JB02000A)

タイトルに関連する用語 (3件)： 計量 ,  理論 ,  公理