2024.02.09
https://gyazo.com/0b4274b7fb6ea27234a4f3a678971075
倫理ツー
前:
2024.02.08
後:
2024.02.10
#日報
観た
ゆるゆり
を6話あたりまで観た.
全部音MADと東方手書きパロで見たことある!
結構ダイナミックな動きで面白い.
思った
【高音質】音楽.mp3
が割と大所帯になってたし,このあいだおれがいないけど普通に回ってた.
メモ
M. Maggesi, C. P. Brogi; "Mechanising Gödel–Löb Provability Logic in HOL Light"
のコードがどこにあるのかよく分かっていなかったが,
なんと
HOL Light
のメインリポジトリに存在する:
https://github.com/jrh13/hol-light/tree/master/GL
意外性有りすぎる
チラ読みした感じ,
ラベル付きシークエント計算
も形式化して
$ \bf GL
の自動証明/
証明探索
とかも実装してるっぽい.
エーッ
ところで
HOL Light
の証明読みづらすぎる.
メモ
Lean 4
の
WellFounded
は使いづらく,
$ \bf GL
の無限上昇列が存在しない/整礎性は自前で関係を定義することになってしまった…