このエントリは Theorem Prover Advent Calendar 2015 - Qiita の 23 日目です。 とは言ってみたものの、内容はいわゆる定理証明器の話ではありません。モデル検査器 Alloy を利用して古典命題論理のシークエント計算をモデル化し、証明図を自動生成させるこ…