Building Bridges between Symbolic Computation and Satisfiability Checking http://dl.acm.org/citation.cfm?id=2756636 を読んだ。(via https://twitter.com/ikegami__/status/616740994143387648 )

計算代数の分野と、SAT/SMTの分野は割と独立して発展してきていて、それぞれ異なる特徴があるけれど、組み合わせていきたいね、というような話。自分も「SAT問題と他の制約問題との相互発展」 http://dx.doi.org/10.11309/jssst.32.1_103 で書いたけれど、SAT/SMTと計算機代数や数理最適化を含む色々な分野の間にそういう関係が色々とあり、組み合わせて色々と面白いことをやっていきたいねぇ。

余談ながら、計算機代数について言うと、自分が計算機代数周りのことを少し勉強＆実装して、Haskellで計算機代数勉強会 <http://partake.in/events/451a51b0-b18e-4e01-bda4-423bf57f4051> で紹介したりしたのは、そういったことが出来たら面白そうという思いもあった。ただ、その後、Dejan Jovanović 氏らの http://research.microsoft.com/pubs/159549/nonlinear.pdf とかを読んで、ヤラレタと思ったのだけれど。

そんなこんなで、この論文の話は大体は知っている話だったけれど、 この著者らの作っている SMT-RAT (SMT Real-Arithmetic Toolbox) http://smtrat.github.io/ は知らなった。

あと、計算機代数的なもののことを symbolic computation と言っていてちょっとだけ驚いた。自分の場合 symbolic computation という言葉からは、むしろ純粋に記号操作的な定理証明器のイメージが想起されたので。 まあ、考えてみたら The International Symposium on Symbolic and Algebraic Computation (ISSAC) という会議名からしてそうだし、やっぱりちょっとコミュニティの違いを感じるね。でも、この Erika Ábrahám さん、ハイブリッドシステムのモデル検査とかやってる人っぽいけれど…… (^^;