Checkable Proofs for First-Order Theorem Proving http://www.cs.man.ac.uk/~regerg/arcade/papers/paper_19.pdf ARCADE 2017 の発表で、一階述語論理の自動証明向けにもSATにおけるDRATのような証明フォーマットを作っていくべきという話。
具体的には以下のような要件を満たしたい。
・Generality: 高い表現力
・Preprocessing and “unsound” steps: 論理的には健全でない前処理なども表現可能
・Efficiency: 効率的な検証が可能 (低次の多項式時間で)
・Easy implementation and low overhead: 実装が容易で証明器のオーバーヘッドが小さいこと
・General adoption: 多くのツールで採用されていること
既にTSTPフォーマットはあるが、規則名や意味論が標準化されていないという問題がある。
また、SMTコミュニティでも既に試みがあり、
・自動証明器の論理はSMTにおける(量化子付きの) uninterpreted function の理論に包含される
・ATPを様々な理論をサポートするよう拡張する試みもある
・プログラム解析やプログラム検証といった共通の応用先では同じフォーマットだと嬉しい
ことから、特にSMTコミュニティにおける展開を密接に追っていくと良いのではとのこと。
SMTにおける証明フォーマットはSMT-LIBではまだS式という以上の標準化はされていないのだけれど、色々と試みがあるのね。 個人的にはZ3以外のソルバの証明フォーマットを知らなかったので、ほほう、と思った。
【参考】
・The Potential of Interference-Based Proof Systems
https://plus.google.com/+MasahiroSakai/posts/DuxckMT4fm5
・Proofs and refutations, and Z3
http://research.microsoft.com/en-us/um/people/leonardo/iwil08.pdf
・Z3の証明の可視化の試み
https://plus.google.com/+MasahiroSakai/posts/c993VVntJQ6
https://plus.google.com/+MasahiroSakai/posts/3VgnRvgaE4n
https://plus.google.com/+MasahiroSakai/posts/4Q8gcmRKPD6