曖昧な用語法：典型的な例

Isabelleの場合：

• 定理： 実装言語MLのデータ型thmとそのインスタンスを定理と呼び、それに引きずられている。実装レベルでは、たいていの概念がthmデータで表現されているので、なんでも定理（＝thm）となる。
• ルール： オブジェクト論理（ユーザー定義の論理）の基本推論規則を、メタ論理（Pure）の公理として埋め込むので、ルールと公理の区別が曖昧になる。さらにルールも公理もthmデータなので定理である。
• ゴール： 実装上の概念。これもthmデータ＝定理である。さらに、ゴールのデータ構造がツリーなので、ツリー用語の曖昧性が加わる。

ツリー用語の曖昧性は：

• ノードと、そのノードを相対ルートとするサブツリーが区別されない。
• サブツリーの種類として、フルサブツリーか一般の（フルとは限らない）サブツリーかがたいてい曖昧。
• サブツリーがリーフを共有するかそうでないかが曖昧。

ゴールに関しては：

• ゴールはツリー構造である
• ゴールツリーのルートノードをゴールと呼ぶことがある。
• 特定のゴールノードに対して、その子ノードを、サブゴールと呼ぶ。
• ゴールはツリーあるいはサブツリーの意味もあるので、サブゴールはサブツリーを意味することがある。
• サブツリーは複数あり得るので、子ノードリストとサブツリーヘッジの区別が曖昧になる。
• 結局、ゴール（単数形）の意味は、
  1. ツリー全体
  2. ツリーのルートノード
  3. サブツリー
  4. サブツリーのルート
• サブゴール（単数）が全体のルートのこともある。これはUIのラベルがsubgoalsである影響からだろう。したがって、ゴールとサブゴールの区別は曖昧。
• サブゴールズ（複数）はノードリストか、サブツリーのヘッジかは曖昧。
• 結果的に、ほとんどまったく意味不明となる。