文献

J-GLOBAL ID：202102271636438982   整理番号：21A2711943

CSEE 1.0:1次論理のための統合型自動定理証明器【JST・京大機械翻訳】

CSE_E 1.0: An Integrated Automated Theorem Prover for First-Order Logic

著者 (10件)： Cao Feng (School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China) ,  Cao Feng (National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China) ,  Xu Yang (National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China) ,  Xu Yang (School of Mathematics, Southwest Jiaotong University, Chengdu 610031, China) ,  Liu Jun (National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China) ,  Liu Jun (School of Computing, Ulster University, Belfast BT37 0QB , Northern Ireland, UK) ,  Chen Shuwei (National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China) ,  Chen Shuwei (School of Mathematics, Southwest Jiaotong University, Chengdu 610031, China) ,  Ning Xinran (School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China) ,  Ning Xinran (National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China)
資料名： Symmetry (Web)  (Symmetry (Web))
巻： 11  号： 9  ページ： 1142  発行年： 2019年 
JST資料番号： U7282A  ISSN： 2073-8994  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： スイス (CHE)  言語： 英語 (EN)

抄録/ポイント： 一次論理は数学的論理の重要な部分であり,自動化定理証明は数学とコンピュータ科学の学際的分野である。本論文は,CSEが,一次論理とEの最近導入されたマルチクラス標準矛盾分離(S-CS)計算に基づく,C_S E_E1.0と呼ぶ,一次論理のための自動定理証明器を提示して,そこでは,一次論理とEのための,最近導入されたマルチクラス標準矛盾分離(S-CS)計算に基づく,重合せと書き換えに基づく一次論理のためのよく知られた方程式定理証明器である。組合せ証明者C S E_E1.0の動機は,(1)C S E_Eの能力,適用性および普遍性を評価し,(2)CSEの新しいマルチクラスS-CS動的演繹とEの成熟等値処理を利用して,ますます困難な問題を解決することである。Eの他の改良とは対照的に,C S E_E1.0は,主に推論機構の観点からEを最適化する。本研究の焦点を,S-CS規則,発見的戦略,および実装のためのS-CS動的推論アルゴリズムを含むC S E_Eの記述に与えた。組合せに関して,Eの能力を失いなくて,C S E_Eを使用して,Eによって未解決であるいくつかのハード問題を解決するために,C S E_E1.0は,時間において2つの証明器の運転をスケジュールした。プレーンEを最初に実行して,もしEが証明を発見しないならば,それは単純なCSEを実行せず,次に,それは証明を見つけなければなら,次に,補題としてCSEランで推論されたいくつかの節理を,オリジナルの節理セットに追加し,そして,更なる証明探索のために,組み合わせ節理セットをEに戻した。C S E_E1.0を,ベンチマーク,例えばCASC-26(2017)とCASC-J9(2018)競争問題(FOF分割)を通して評価した。実験結果は,C S E_E1.0が確かにEの性能を強化することを示した。Copyright 2021 The Author(s) All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  最適化 ,  自動化 ,  計算機科学 ,  節理 ,  適応性 ,  *定理証明 ,  重合せ ,  境界領域 ,  ベンチマーク ,  推論マシン ,  普遍性 ,  演繹
準シソーラス用語： *自動定理証明 ,  補題 , 【Automatic Indexing@JST】

著者キーワード (6件)： 定理証明器 ,  一次論理 ,  標準矛盾分離 ,  重合せ ,  マルチクラウス ,  推論機構

分類 (2件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R)

引用文献 (40件)：

• Pavlov, V.; Schukin, A.; Cherkasova, T. Exploring Automated Reasoning in First-Order Logic: Tools, Techniques and Application Areas. In Proceedings of the 4th International Conference on Knowledge Engineering and the Semantic Web, St. Petersburg, Russia, 7-9 October 2013; pp. 102-116.
• Kovacs, L.; Voronkov, A. Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering, York, UK, 22-29 March 2009; pp. 470-485.
• Nipkow, T.; Brinkop, H. Amortized Complexity Verified. J. Autom. Reason. 2019, 62, 367-391.
• Sutcliffe, G. The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 2017, 59, 483-502.
• TSTP Solution Domains. Available online: http://www.tptp.org/cgi-bin/SeeTPTP?Category=Solutions (accessed on 16 May 2019). CASC Solution Domains. Available online: http://tptp.org/CASC/ (accessed on 16 May 2019).

タイトルに関連する用語 (3件)： 論理 ,  統合 ,  自動定理証明