自動定理証明紹介 Proof Summit 20110925酒井 政裕自己紹介酒井 政裕 Blog: Twitter: masahiro_sakai Haskeller Agda: Agda1遊 Coq: 最近入門 最近、 Alloy本翻訳Alloy本抽象設計Alloy形式手法 社好評発売中！ LT趣旨Coq Agda話、 息抜 違話話自動定理証明Automated Theorem Proving発見色 Decision procedureSAT/SMTCoq Agda 自分考証明形式化、正確認、便利 、何証明、本当支援 ?Coq Agda機械分、細部証明書機械奴隷 ?対話的定理証明 vs 自動定理証明対話的定理証明 自動定理証明 Coq, Agda, E, SPASS, Otter, 自動化 人間証明書、検査。証明探索。人間古典論理 ? 直観主義論理 古典論理高階 /一階 高階 一階多分辺Comparing mathematical provers(by Freek Wiedijk, 2003) 数学的表現力弱、分自動化！
