はじめに マイクロソフト・リサーチが開発しているz3定理証明器に興味を持ったのでそれについてです。 鶴亀算 まずはオンラインのコンソールで鶴亀算を解いてみましょう。 z3はSMT-LIB標準形式のバージョン2を解釈できるのでそれを用いて鶴亀算の各制約を記…