PLP のプログラムが成功するとき、論理式として見ると証明図を書くことができることを帰納法で証明していきます。 となる に関する帰納法で証明します。 から始めます。PLP のプログラムは1個の述語式から始めると定義したので、 のときは書くことができませ…

ここでは は単に項 と が一致するとき true 、そうではないとき false となるものとします。 を述語式で表す方法については後で述べる予定です。Prolog の単一化についても後で述べる予定です。 プログラムが成功するときは、論理式として見ると証明図を書く…