文献

J-GLOBAL ID：201102296031022076   整理番号：11A1196000

帰謬法含意に基づく一次論理で最小充足不可下位式を抽出するためのアルゴリズム

An Algorithm for Extracting Minimal Unsatisfiable Subformulae in First-Order Logic Based on Refutation Implication

著者 (3件)： ZHANG Jian-Min (School of Computer,National Univ. of Defense Technol., Hunan, Changsha) ,  SHEN Sheng-Yu (School of Computer,National Univ. of Defense Technol., Hunan, Changsha) ,  LI Si-Kun (School of Computer,National Univ. of Defense Technol., Hunan, Changsha)
資料名： Jisuanji Xuebao  (Jisuanji Xuebao)
巻： 33  号： 3  ページ： 415-426  発行年： 2010年 
JST資料番号： C2531A  ISSN： 0254-4164  CODEN： JIXUDT  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： 公式の「実行不可能性」の原因について説明するのにおいて,ソフトウェア検証や分析などのように,多岐での理論上的,そして,実際的応用がある。最小充足不可下位式は実行不可能性の簡潔な説明を提供し,そして,急速に間違いを発見する自動ツールを助け,急速に間違いを発見し,そして,失敗の基本的理由を決定できる。著者らは論破含意グラフとその前進の,そして,後方の届いている頭頂の定義,および最小充足不可下位式と論破含意グラフと関係を導入する。関係に基づいて,作者はコンフリクト解析と論破含意に基づくアルゴリズムを提案する。そこでは,論破含意グラフ刈り込みと呼ばれるテクニックを,実施する。実用的ベンチマークの実験結果は,提案したアルゴリズムが最初に深さ検索アルゴリズムより優れていることを示している。公式が,より複雑になっているが,アルゴリズムは最初に深さ検索アルゴリズムよりはるかに速い。Data from the ScienceChina, LCAS. Translated by JST

シソーラス用語： *アルゴリズム ,  *論理 ,  含意 ,  プログラム検証 ,  計算機アルゴリズム ,  ベンチマーク ,  葛藤 ,  実用化
準シソーラス用語： コンフリクト ,  ソフトウェア検証 ,  検索アルゴリズム ,  実験結果 ,  実際的応用

分類 (1件)： 人工知能  (JE08000Z)

タイトルに関連する用語 (4件)： 含意 ,  論理 ,  充足 ,  アルゴリズム