定理証明支援系での論理の形式化 - Internet Explorer 2.0

定理証明支援系での論理の形式化

メモ

予定としては，このリストにまとめて行く．

https://iehality.github.io/lean4-logic/book/references.html#lean-4

Towards a Coq formalization of a quantified modal logic

Lubor Budaj; "Formalization of modal logic S5 in the Coq proof assistant"

https://fse.studenttheses.ub.rug.nl/28482/1/BSc_Thesis_final.pdf

Minchao Wu, Rajeev Goré; "Verified Decision Procedures for Modal Logics"

Yiming Xu, "Formalizing Modal Logic in HOL"

Lawrence C. Paulson; "A Mechanised Proof of Gödel’s Incompleteness Theorems using Nominal Isabelle"

M. Maggesi, C. P. Brogi; "A Formal Proof of Modal Completeness for Provability Logic"

Lean

iehality/lean-logic

FormalizedFormalLogic/Foundation

Bruno Bentzen; "A Henkin-style completeness proof for the modal logic S5"

Paula Neeley; "A Formalization of Dynamic Epistemic Logic"

https://paulaneeley.com/wp-content/uploads/2021/05/draft1.pdf

実装: https://github.com/paulaneeley/modal

https://github.com/ljt12138/Formalization-PAL

https://github.com/alexoltean61/hybrid_logic_lean

Coq

Coqによる分離論理の形式化