問題タブ [successor-arithmetics]

証明が不完全な次のレンマがあります。

この証明は失敗します

これeq_Sを証明する方法のようですが、適用できません（:n + 1として認識されません）。も試しましたが、関係が見つかりません。を使用すると、同じ最終目標になります。S nError: Unable to find an instance for the variable y.ringrewrite

どうすればこの証明を完成させることができますか?

知識ベース

クエリ

痕跡

私の質問

• 節 2 の再帰呼び出しが、引数 1 の各呼び出しで最も外側の succ() を取り除く方法がわかります。
• 各呼び出しで引数 3 に外側の succ() を追加する方法がわかります。
• これらの再帰呼び出しの結果として、第 1 引数がいつ 0 になるかがわかります。その時点で、第 1 節が第 2 引数を第 3 引数にどのようにコピーするかがわかります。

これは私が混乱するところです。

1. 最初の節が実行されると、2 番目の節も自動的に実行され、最初の引数に succ() が追加されますか?

2. また、プログラムはどのように終了するのですか? また、最初と 3 番目の引数に succ() を無限に追加し続けないのはなぜですか?

LearnPrologNow.com からの説明 (わかりません)

Prolog がこのクエリを処理する方法を順を追って見ていきましょう。クエリのトレースと検索ツリーを以下に示します。

最初の引数は 0 ではありません。これは、add/3 の 2 番目の句のみを使用できることを意味します。これは、 add/3 の再帰呼び出しにつながります。最も外側の succ ファンクターは、元のクエリの最初の引数から取り除かれ、その結果が再帰クエリの最初の引数になります。2 番目の引数は変更されずに再帰クエリに渡され、再帰クエリの 3 番目の引数は変数 (以下に示すトレースの内部変数 _G648) です。_G648 はまだインスタンス化されていないことに注意してください。ただし、クエリが 2 番目の句のヘッドと統合されたときに R が succ(_G648) にインスタンス化されたため、R (元のクエリで 3 番目の引数として使用した変数) と値を共有します。しかし、これは R が完全にインスタンス化されていない変数ではなくなったことを意味します。複雑な用語になってきましたが、

次の 2 つの手順は基本的に同じです。すべてのステップで、最初の引数は成功の 1 つの層になります。以下に示すトレースと検索ツリーの両方がこれをうまく示しています。同時に、すべてのステップで succ ファンクターが R に追加されますが、常に最も内側の変数はインスタンス化されません。最初の再帰呼び出しの後、R は succ(_G648) です。2 回目の再帰呼び出しの後、_G648 は succ(_G650) でインスタンス化されるため、R は succ(succ(_G650) になります。3 回目の再帰呼び出しの後、_G650 は succ(_G652) でインスタンス化されるため、R は succ(succ(succ() になります。 _G652))) . 検索ツリーは、この段階的なインスタンス化を示しています。

この段階で、すべての succ ファンクターは最初の引数から取り除かれ、基本節を適用できます。3 番目の引数は 2 番目の引数と同等であるため、複素項 R の「穴」(インスタンス化されていない変数) は最終的に埋められ、完了です。

Prologで自然数から後継数を作りたい。

出力は次のようになります。

実は無限ループです。結果としてtrueになるだけでなく、ループを終了する方法はありません。

まず第一に、私はプロローグがまったく初めてで、M が X よりも N と異なる場合に真である述語 length(M,X,N) を書き込もうとしています。

M(=dec.5) と N(=dec.2) が X(=dec.2) より大きく異なる場合に真となる次のテストケースを作成しました。5 と 2 の差は 3 で、2 より大きいため、この場合は真です。

私はプロローグが再帰的に機能することを知っているので、C のような言語のように条件 (<,> など) を使用してそのような述語を構築できるかどうか、またはプロローグでこれを行う別の方法があるかどうか疑問に思っています。この単純な質問で申し訳ありませんが、プロローグを始めたばかりです。