知識ベースと半形式性

知識ベースには、次のようなものが入っている。

1. 型の宣言・定義
2. 関数の宣言・定義
3. 命題の宣言・定義
4. 導出の宣言・定義
5. リーズニングの宣言・定義
6. メタリーズニングの宣言・定義
7. それらを組織化する構造ファセット

知識ベースを背景にして、新しい型／関数／導出／リーズニングを構成する行為が広義の計算。

このとき、半形式的記述の特徴は：

1. あいまい検索： 知識ベースの特定のアイテム（宣言、定義、指標など）を検索する際に、曖昧指定でもなんとかなる。表記のゆれ（漢字かひらがなか、大文字小文字、人名表記、助詞のあるなし、etc.）や常識的な別名は許容される。また、文脈も考慮される -- 「オイラーの定理」が何を意味するか？ とか。
2. パターンマッチング〈ユニフィケーション〉： 書き換えアクションの適用可能性〈applicability〉の判定にパターンマッチングが使われる。
3. 暗黙の了解： パラメータを明示的に指定しなくても推測する。
4. 後回しと前方参照： 一部の計算・証明を後回しにして、名前だけ付けておくことが出来る。
5. 先行名付け： まだ定義してないものに名前を付ける。名付けの正当性証明の義務が発生する。