2024.04.05
https://www.youtube.com/watch?v=-1CSTFH2Xjw
観た
ワッツ
ホロ萌えすぎ
メモ
知った
知った
そもそもIsabelleというのは、ある種のメタ論理(metalogic; logical framework)を提供している本体部分があり、そこに基底型や関数記号、公理を追加することで様々な対象論理(object logic)を表現している。対象論理の例として、高階論理(Isabelle/HOL)や1階論理(Isabelle/FOL)、ZF集合論(Isabelle/ZF)などがあり、その中で一番使われているのがIsabelle/HOLである。 思った
$ \Box^nや$ \Diamond^nといったあまり本質的でない略記にめちゃくちゃ時間を取られ気が狂う