定理証明支援システムCoqの勉強会です。

• Lambda Prologのチュートリアル (Coq-ELPI) を読みます。

https://github.com/LPCIC/coq-elpi/tree/master/examples

(和訳） https://gitlab.com/proofcafe/elpi/-/blob/main/tutorial_elpi_lang_jp.v

https://qiita.com/suharahiromichi/private/62fd01d0000b29156d2e

pi x\ と => から。

• Coq-Elpi によるタクティクの作成

https://github.com/suharahiromichi/coq/blob/master/elpi/coq_elpi_tactic_sample_1_2.v

• 論理としてのProlog

https://github.com/suharahiromichi/coq/blob/master/ssr/ssr_prolog_in_logic.v

参加をご希望のかたは、管理者までお問い合わせください。

可能ならば coq-mathcomp を事前にインストールしておいてください。

一部資料は非公開なので、参照には gitlab のアカウントを用意してください。

以上