エルブラン解釈

通常、論理式の中の変数には「自然数」や「人間」などの意味を与えますが、コンピュータは意味を理解できません。

そこで領域を 「記号（文字列）の集合」に固定し、意味の計算を放棄して、ただの構文（文字列のパターンマッチ）だけで論理の正しさを判定する枠組みが エルブラン解釈です。

具体的には、エルブラン宇宙（定数・関数で組み立てられるすべての項）の要素を使って作れる「変数を持たない述語」のリスト（アトム集合）を作り、それに機械的に真偽を割り当てます。

下のジェネレータでは、定数・関数・述語を入力するとアトムを 30 件ずつ遅延生成します。 スクロールするほどリストは膨らみます。これはあくまで「組み立て」であり、意味の計算は一切していません。