あっ、そういうこと!?

propositin, fact, goal と並べて書いてあるのを見て、ひょっとして、と思った。

• propositionとは、真偽の判定を伴わない単なるexpression、つまり論理式のこと
• factとは、propositionに |- のマークが付いたもの。つまり、判断主張文。
• goalとは、propositionに ?- のマークが付いたもの。つまり、問題提示文。

「判断主張文 vs 問題提示文」という発想と組み合わせると、fact vs goal で辻褄が合う。

これと、propositionとルールの関係、つまり「オブジェクト論理のルールをPureのpropositionで表現する」と組み合わせろと、だいたいの曖昧性を表現出来る気がする。

1. propositonとformulaは同義である。特に区別しない。（ただし、真偽値としてのpropは別）
2. 既に証明済み、または一時的に仮定する、によりpropositionはfactとしてマークされる。
3. これから証明する、とマークされたproposition（＝formula）をgoalと呼ぶ。
4. リーズニングステップは、証明メソッドで遂行される。
5. rule系メソッドは、ルールを参照する。
6. このルールはオブジェクト論理の推論ルールであり、Pureのfact（定理か仮定）である。
7. よって、ルールと定理を混同して使う。

曖昧な言い方の解釈を示す。

1. ルールは定理である → オブジェクト論理のルールは、Pureの公理として表現する。公理は定理の一種であり、いずれにしてもthmデータである。
2. ゴールは定理である → ゴールは ?- とマークされた論理式（＝命題）である。論理式はthmデータである。
3. 定理はルールである (1) → Pureの定理（公理を含む）の一部はオブジェクト論理のルールの表現になっている。
4. 定理はルールである (2) → オブジェクト論理Aは、⇒A という形の推論ルール（派生ルール）とみなせる。
5. ファクトは定理である → ファクトと定理（証明済みの命題（＝論理式））は同義としても使う。
6. ファクトはコンテキストである → 正確には、ファクトはコンテキストの要素、またはコンテキストの部分集合である。
7. コンテキストはセオリーである → セオリーの定義として、論理系の論理式の集合とする定義がある。コンテキストは論理式の集合だから、セオリーと言える。