前回の続き。論理式をAgdaで証明していくのですが、実際にコードを書く前に論理式とはどうやって証明すればいいかのお話。 推論規則 論証の妥当性を示すのに用いられる規則を推論規則と呼ぶ。以下は推論規則をを用いて論証の妥当性を示すための規則である。 …

今回大学の講義で使用したAgdaについての紹介です。 そもそもAgdaとは？wikiによると Agdaは定理証明器、すなわち数学的な証明を検証するコンピュータプログラムである （中略） 他の定理証明支援系ではスクリプトによって「戦略」を指定して証明を操作する…