リーズニング、ファクト、チェーン

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

証明オブジェクトを作る過程をリーズニングと呼ぶことにする。リーズニングは、それまでに知られていた知識・情報を変形したり追加することの連鎖だと言える。この連鎖をチェーンと呼ぶ。チェーンのあいだで受け渡される知識・情報がファクトってことだろう。

チェーンが、示すべき結論から出発するならバックワードチェーン、既に示されている（あるいは仮定されている）前提から出発するならフォーワードチェーン。

実際のリーズニング（証明の構成過程）では、チェーンは行ったり来たりするのでバイダイレクショナルとなる。