文献

J-GLOBAL ID：201902285340613869   整理番号：19A2828220

Vampireにおける飽和試行の対話型可視化【JST・京大機械翻訳】

Interactive Visualization of Saturation Attempts in Vampire

著者 (4件)： Gleiss Bernhard (TU Wien, Vienna, Austria) ,  Kovacs Laura (TU Wien, Vienna, Austria) ,  Kovacs Laura (Chalmers University of Technology, Gothenburg, Sweden) ,  Schnedlitz Lena (TU Wien, Vienna, Austria)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 11918  ページ： 504-513  発行年： 2019年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 形式的方法の多くの応用は,システムの安全性やセキュリティなどのシステム特性に関する自動推論を必要とする。自動推論エンジンの性能を改善するために,SAT/SMTソルバと一次定理証明器のような,論理的証明やモデルのような形式的証明書を生成するために,これらのエンジンの成功と失敗の両方を理解する必要がある。このような解析は,証明/モデル探索中に生成される多数の論理式により困難である。本論文では,飽和ベースの一次定理証明に焦点を当て,一次定理証明における飽和ベースの証明試みを対話的に可視化するためのSatVisツールを導入した。SatVisにおけるVampireの飽和試みを対話的に可視化することにより,世界主導定理プローバVampireのトップにSatVisを構築した。本研究では,対話型変換と探索機能を持つ飽和試みにより誘導された誘導グラフの自動レイアウトと可視化を組み合わせた。結果として,Vampireの証明を分析しデバッグすることができた。その対話的可視化のおかげで,SatVisは一次証明を理解し,一次証明書の証明を解析/洗練するための定理において専門家と非専門家の両方を助けると信じる。Copyright 2019 Springer Nature Switzerland AG Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 会話 ,  *可視化 ,  定理証明 ,  システム特性 ,  セキュリティ
準シソーラス用語： 対話型 ,  論理式 ,  証明書 ,  ソルバ , 【Automatic Indexing@JST】

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

タイトルに関連する用語 (3件)： 飽和 ,  試行 ,  対話型可視化