日々の流転

λ. Omega test and beyond

ProofSummit2012 にて、Omega test and beyond という題での発表を行いました。内容は Coq の omega タクティック他で広く使われている Omega test という決定手続きの概要とその周辺の簡単な紹介です。Keynote使うのが初めてだったので、スライド作りにはちょっと苦戦してしまった。

資料 (PDF, Keynote)

関連

• ProofSummit2012 - Togetter
• 昨年のProofSummit2011での発表(LT)「自動定理証明の紹介」

λ. How a CDCL SAT solver works

1年くらい前に、知人にSATソルバの動作を説明しようとして、ちょうど良い資料がなくて、紙で頑張って説明したのを、スライド化してみた。 単純な分割統治による探索とはちょっと違った動作になっているのが分かると思う。

資料 (PDF, Keynote)

参考図書