1.7.2 実行は証明過程, 計算結果は反例

このように節を公理に対応づけると, KL1 のプログラムの実行過程は, トップ レベルに与えられた命題の証明過程であると考えることができる. たとえば, 以下のようなメインプログラムを考える.

main :- a([1,2], [3,4,5], L).

つまり「どんな をもってきても, それに対して は成り立たない」, いい換えれば「 と を結合したようなものは存在しない」という意味である. プログラムの実行 は, この命題が成り立たないことを証明する過程である.

ある命題を成り立たないことを証明するには, 反例をあげれば良い. 論理型 言語による計算とは, この反例を見つけることである. その反例自身が計算 の結果になっている. 上記の append の場合なら, の反例, すなわち を満たす を見つけてやれば良い. これは, と を結合したらどんなリストになるかを計算していることに他ならない.

KL1 や Prolog が属するホーン論理に基づく論理型言語では, 反証したい命題 から始めてトップダウンに, 公理を用いてブレークダウンしていく方法でこの 証明を行なう. このようなやり方を後向き推論 (backward reasoning) など とも呼ぶ.実 際の証明手続きをちょっと追ってみると, 以下のようになる.

1.   公理である (1.2) から

    

   が成り立つような があれば, が元の命題 (1.3) の反例になっていることがわかる. そこで, 命題 (1.4) を満たすような がないか探すことにする.

2. ステップ 1) とまったく同様に (1.2) から

    

   を満たすような があれば, が命題 (1.4) を成立させるような例になっていることがわかる. そこで, こんどは (1.5) を満たすような がないか探すことにする.

3. 公理 (1.1) によって, としたら, (1.5) が成り立つことがわかる.