研究実績の概要 |
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 における証明項の取り出しの実装的複雑さなどにより、十分な形式証明の実装は進んでいないが、今後、継続して続ける予定である。
|