「プログラマー向けの（？）数理論理学」のまとめページです。更新履歴や関連情報なども掲載します。
進捗状況
あまり良くありません。今後更新頻度が落ちるかもしれません。
連載一覧
- プログラマー向けの（？）数理論理学（１）数学的言明
- プログラマー向けの（？）数理論理学（２）証明と推論規則と仮定
- プログラマー向けの（？）数理論理学（３）ウェブアプリ化
- プログラマー向けの（？）数理論理学（４）証明図
- プログラマー向けの（？）数理論理学（５）含意のみに関する主要な定理
- プログラマー向けの（？）数理論理学（６）否定に関する推論規則
- プログラマー向けの（？）数理論理学（７）連言に関する推論規則
- プログラマー向けの（？）数理論理学（８）選言に関する推論規則
- プログラマー向けの（？）数理論理学（９）同値に関する推論規則（予定）
- プログラマー向けの（？）数理論理学（１０）推論規則コマンドの追加等（予定）
- プログラマー向けの（？）数理論理学（１１）否定と含意に関する主要な定理（予定）
- プログラマー向けの（？）数理論理学（１２）連言に関する主要な定理（予定）
- プログラマー向けの（？）数理論理学（１３）選言に関する主要な定理（予定）
- プログラマー向けの（？）数理論理学（１４）同値に関する主要な定理（予定）
- プログラマー向けの（？）数理論理学（１５）命題論理のその他の主要な定理（予定）
- プログラマー向けの（？）数理論理学（１６）カテゴリー機能（予定）
- プログラマー向けの（？）数理論理学（１７）証明図の画像保存（予定）
- プログラマー向けの（？）数理論理学（１８）論理式のパーサ（予定）
- プログラマー向けの（？）数理論理学（１９）正規化（予定）
- プログラマー向けの（？）数理論理学（２０）述語論理（予定）
- プログラマー向けの（？）数理論理学（２１）述語論理の推論規則（予定）
- プログラマー向けの（？）数理論理学（２２）代入に関する推論規則（予定）
関連記事
数学ゲーム（定理証明ゲーム）を作ろう（１）構想を練ってみる（予定）
今後取り扱うかもしれないこと
数学
- 述語論理
- 公理的集合論
- .etc
機能追加・改善
- 論理式のパーサ作成
- 証明図上で直接証明を作成する機能
- 数学記述言語の作成
- ログイン機能
- 公開機能
- メタデータ追加
- 1つの数学的命題に対する複数の証明の扱い
関連情報
GitHub
「rena」という名称で公開しています。
https://github.com/pizyumi/rena
近々Twitterでも形式化数学の情報（様々な定理の形式的証明など）や開発の進捗状況を発信していきたいと思っています。
ウェブページ
まだまだ先になりそうですが、形式化数学に関するウェブページを作成したいです。
更新履歴
2019/1/26
- （８）選言に関する推論規則・・・投稿
2018/12/3
- （７）連言に関する推論規則・・・投稿
2018/11/30
- （６）否定に関する推論規則・・・投稿
2018/11/26
- （５）含意のみに関する主要な定理・・・投稿
2018/11/23
- （４）証明図・・・証明図のCSSとHTMLを変更
- （４）証明図・・・証明図作成のロジックを大幅に改良・バグ修正
- （４）証明図・・・説明の詳細化
2018/11/22
- （２）証明と推論規則と仮定・・・含意導入規則のロジックを大幅に改良
- （２）証明と推論規則と仮定・・・説明の詳細化
2018/11/12
- （４）証明図・・・投稿
2018/11/9
- （２）証明と推論規則と仮定・・・説明追加
- （３）ウェブアプリ化・・・投稿
2018/11/7
- （２）証明と推論規則と仮定・・・投稿
2018/11/6
- （１）数学的言明・・・投稿