現状報告

• fact(s) -- まだ謎。おそらくは、contextと同義。
• constant -- 狭義の定数記号だけではなく、関数記号、関係記号、述語記号、定理に付けられたラベルなどは定数と呼ぶ。高階論理なので、関数、述語、関係なども意味領域のモノ（個体）となるから、定数と呼んでもいい。命題もモノだから、命題（定理）の名前も定数だ。けど、型定数はconstantとは呼ばないのかも。
• result -- 昔のIsabelleのresultコマンド（ML関数）の機能を意識しているのだろう。リーズニングが成功したときに、その時点の証明状態から取り出せるデータ構造。
• theorem -- カオス。MLのthmデータをイメージしているから、何でもtheoremになる。また、ルールやゴールもtheoremだ、とも言っている。
• goal -- ツリー構造を非常にイイカゲンに表現したいときにイイカゲンに使うイイカゲンな言葉。真面目にとり合ってもショウガナイ。