興味深い質問がありますが、正確にどのように表現すればよいかわかりません...
ラムダ計算を考えてみましょう。与えられたラムダ式に対して、いくつかの可能な削減順序があります。しかし、これらの中には終了しないものもあれば、終了するものもあります。
ラムダ計算では、1つの特定の還元次数があり、それが実際に存在する場合、常に既約解で終了することが保証されていることがわかります。それは通常の順序と呼ばれます。
簡単なロジックソルバーを作成しました。しかし、問題は、制約を処理する順序が、解決策を見つけるかどうかに大きな影響を与えるように見えることです。基本的に、私の論理プログラミング言語には通常の順序のようなものが存在するかどうか疑問に思っています。（または、単なるマシンでこの問題を決定論的に解決することは不可能かどうか。）
それが私が求めているものです。おそらく、答えは「単純な論理ソルバー」が何であるかによって大きく異なります。それで、簡単に説明しようと思います。
私のプログラムは、 The Fun of Programming（Jeremy Gibbons＆Oege de Moor）の第9章にあるコンビネータのシステムに密接に基づいています。言語の構造は次のとおりです。
ソルバーへの入力は単一の述語です。述語には変数が含まれる場合があります。ソルバーからの出力は、0個以上の解です。解決策は、述語を真にする一連の変数割り当てです。
変数は式を保持します。式は、整数、変数名、または部分式のタプルです。
式（述語ではない）を比較して等価である等式述語があります。すべての（バインドされた）変数をその値で置き換えると、2つの式が同一になります。（特に、すべての変数は、バインドされているかどうかに関係なく、それ自体と等しくなります。）この述語は、統合を使用して解決されます。
ANDとORの演算子もあり、これらは明白な方法で機能します。NOT演算子はありません。
基本的にローカル変数を作成する「exists」演算子があります。
名前付き述部を定義する機能により、再帰的なループが可能になります。
論理プログラミングの「興味深い点」の1つは、名前付き述語を作成すると、通常は前後方向（場合によっては横方向）に機能することです。標準的な例：2つのリストを連結する述語を使用して、リストをすべての可能なペアに分割することもできます。
ただし、用語の順序を並べ替えない限り、述語を逆方向に実行すると、検索が無限になることがあります。（たとえば、ANDまたはORのLHSとRHSを交換します。）ソリューションセットが正確に設定されているすべての場合に迅速に終了するために、述語を実行するための最良の順序を検出する自動化された方法があるかどうか疑問に思っています。有限の。
助言がありますか？