https://twitter.com/kinaba のログ (twilog の方が便利です。)
| @septef 退院おめでとうございました。良い写真じゃのう。 | |
| ゲーデルによる「神の存在証明」を、CoqやHOLで形式化・機械化するプロジェクトというの見てた https://t.co/XJ03nDrElv (Coq版) | |
| そもそも元々の公理系の方向性から全然知らなかったので全体像のpdf https://t.co/ZzH9SAwoCN とか割と丸ごと面白い。証明支援系に乗せることで、哲学的機微のある部分の試行錯誤の上に、そこから既存の論理で何が導出できるかは一撃ですっ飛ばして計算できる良さとか |