Isabelleの場合、項としての証明オブジェクトはないし、証明の遂行中の履歴もユーザーから見えている気配がない。その意味で証明オブジェクトの存在は希薄。だが、概念的には何かしらの証明オブジェクトはあるはず。証明オブジェクトを作る過程をリーズニン…

Knowing is not enough,we must apply.Willing is not enough,we must do. だそうで。

isar-refとかimplementtion文書で： stateが状態（名詞）と述べる（提示する、主張する）のときがある。Isar/VMでは、述べるの意味のstateが状態の名前として使われている。"state"という名前で「述べる」の意味のstateがある。 argumentが引数のときと、議…

スレッドをスタートする関数が StartHogeProcess みたいな名前（にしたのは自分）で、プロセスだと思っていて、処理をスタートさせてからメイン側を終了させた。当然にプロセスが終わるので、そのなかのスレッドも終了する。このときの終了の仕方が、かなり…

小野寛晰『情報科学における論理』は、一番よく参照していたと思うが、ない。