2015 Fiscal Year Annual Research Report
形式証明の理論依存性解析とその計算可能証明発見への応用
| Project/Area Number |
25540003
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 形式証明 / 計算的意味 / 項書換え系 / 合流性 / 構成的証明 |
|---|
| Outline of Annual Research Achievements |
H27年度には、未解決問題を含む困難な証明問題について証明構造のケーススタディを進めた。具体的には (1) 1990年に提案された未解決問題である「強無曖昧な右線形項書換え系の合流性」、(2)1981年に Mayr により証明されたが証明が複雑で理解が困難であり、2011年に J.Leroux により提案された簡潔化された新証明 (ACM POPL 2011)が与えられた「ペトリネットの到達可能性の決定可能性」、(3)1980年より未解決問題であった「決定性木語変換器の等価性の決定可能性」（Seidlらにより2015年に肯定的に解決。IEEE FOCS 205)である。これらは(1)は停止順序、(2)は有限基底性、(3)はネーター環の昇鎖列において、存在証明はできても実際のインスタンスの構成ができない、という共通の難しさ（本研究のモチベーション）に起因する。(1)は、いまだ未解決であり、肯定的に解決されるならば、Van Oostrom の減少図手法により必ず適切な停止順序が存在するが、減少図手法は具体的な停止順序の構成法のヒントは与えない。部分的解決として、減少図手法（従来手法）の適用を試みた停止順序の構成に基づく手法（第24回計算機論理国際会議発表）、新手法としてリダクショングラフの有限性に基づく構成的手法（第25回自動推論国際会議発表）を提案した。(2),(3)は、いずれも肯定・否定の双方を探索する二つのセミアルゴリズムを並行して実行することにより、いずれかの成功により判定する。同様の例は、「normed-BPAにおける分岐双模倣の決定可能性」(Fu, ICALP2013)などでも観察されている。結果的には、高階定理証明系 Isabelle/HOL における証明項の取り出しの実装的複雑さなどにより、十分な形式証明の実装は進んでいないが、今後、継続して続ける予定である。
|
| Remarks |
Open induction ライブラリは2013年に形式証明ライブラリ AFP-Openに採録・登録されたが、定理証明系Isabelle/HOLのバージョンアップに伴うメンテナンスを行っている。
|
-
-
-
-
[Presentation] Confluence of Layered Rewrite Systems2015
Author(s)
Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa
Organizer
24th Computer Science Logic 2015 (CSL 2015), LIPICS Vol.41, pp.423-440.
Place of Presentation
ベルリン、ドイツ
Year and Date
2015-09-07 – 2015-09-10
Int'l Joint Research
-
-
