文献

J-GLOBAL ID：201202253758492870   整理番号：12A0581841

証明の灰色領域における演技

Playing in the Grey Area of Proofs

著者 (3件)： HODER Krystof (Univ. Manchester) ,  KOVACS Laura (TU Vienna) ,  VORONKOV Andrei (Univ. Manchester)
資料名： ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages)  (ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages))
巻： 47  号： 1  ページ： 259-271  発行年： 2012年01月 
JST資料番号： D0915A  ISSN： 0362-1340  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 証明から抽出された補間は検証及び静的解析において幾つかの応用を持つ。幾つかの理論において補間が存在する事が保証されているけれども,証明から抽出された補間は一般の補間アルゴリズムによって得られたものと比較して小さくかつ有用である事が判明している。本論文において,筆者らは証明からの補間の抽出及びそのような補間の最小化という2つの関連した問題を考察した。推論の健全性及び局所性双方を保存する証明変換を考察する事によって過去の文献の一般性を利用した。そのような変換は抽出された補間の形状及びサイズを劇的に変えた。筆者らが考察した変換のクラスは明らかに推論の健全性を保存する一方,局所性を侵害し得る。局所性を保存するために,切断の列によって得られる全ての局所証明を符号化する解決であるSAT(充足可能性)問題を生成した。

シソーラス用語： *証明 ,  *抽出 ,  定理 ,  *プログラム検証 ,  推論 ,  健全性 ,  局所性 ,  変換 ,  充足可能性問題
準シソーラス用語： SMTソルバ ,  *最小化 ,  静的解析 ,  *補間

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

タイトルに関連する用語 (3件)： 証明 ,  灰色 ,  演技