The Potential of Interference-Based Proof Systems
おお、これは面白い。 古典的な証明系における推論(inference)はモデルの集合を変化させないのに対し、モデルの集合は保存しないが(un)satisfiabilityを保つような変形をinterferenceと呼び、そのような証明系の研究を提案している。
SATにおけるDRATなどが一番ホットに研究されている領域だけど、著者たちはQSAT(QBF)向けに一般化されたQRATというのも提案していたりとか、最近はDRATよりも更に強力なSPR(set-propagation-redundancy system)やPR(propagation-redundancy system)といったものを提案したりもしてる。 また、一階述語論理、様相論理、分離論理といった他の論理においても、同様の証明系が有用だろうか、といった問も。
最近、 Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer を読んで(https://plus.google.com/+MasahiroSakai/posts/dddK6XDk2A3 )、DRATとかを理解したこともあって、この辺りの話はすごい面白いと思いつつある。 ひょっとしたら、実際的なpreprocessingやinprocessing、unsatisfiabilityのceritificateの生成、それらの基盤となる短い証明が可能かつ証明の検証が容易な証明系、といった一連の話の結びつきは、ここ数年のSAT関係の話の中で一番面白い話かもしれない。
論文: http://www.cs.man.ac.uk/~regerg/arcade/papers/paper_11.pdf
スライド: http://www.cs.utexas.edu/~marijn/talks/interference.pdf