ここまでの説明は, 原則としては KL1 であっても Prolog であっても同じこ とである. 上に述べた証明のステップでは, 証明がうまく進むように, 適当 な公理 (プログラム上では節) を選んでいったので, 一本道の簡単な証明がで きた. しかし, 証明したい命題に適用できる公理が数多くあるもっと複雑な 問題になると, 自動的に適切な公理の選択をすることは不可能である. その ような場合にどうするかが問題になる.
Prolog は, 最初の公理をまず選んで証明を進め, それで行き詰まったら公理 を選ぶところまで後戻りして次の公理を選んでみるという, バックトラッキン グ機構を採り入れた. これで公理の選び方の問題は半分は解決したのだが, とりあえず選んだ公理を用いた証明が, 行き詰まることなく無限ループに入っ てしまうことがあるので, すべての場合でうまく行くわけではない. Prolog のセマンティクスを変えずに並列処理するシステムの研究も行なわれているが, このあたりの方式については基本的には同じである.
バックトラッキングの処理は並列処理との相性があまり良くない. 何人かの グループで, ある方針にしたがって共同作業をしている時に, 行き詰まったか らこれまでやってきた方法は捨てて別の方法でやろう, などと各人が勝手に言っ ているようでは, 到底効率のよい作業はできない. 誰か管理者が全体の作業 状況を見ていて, 一斉に方針変更するように指示を出す, という方針ならもう 少しましになるだろうが, そうやって管理者が把握できる人数は知れている. 計算機による並列処理の場合にも, これと同じような状況が起きる.
そこで KL1 では, どの公理を選ぶかを決めたら決して後戻りしない方針をとっ た. そのかわり, どの公理を選ぶかの条件となる部分を「ガード」として分 離し, その条件を正確に判断できる情報が集まるまでは選択を待つことによっ て, 誤った選択をしないようにしたわけである. このような方針をとる論理 型プログラム言語は, 自らの選択に賭けるというニュアンスから committed choice 型の並列論理型言語などと呼ばれることもある.
Prolog も KL1 も, ホーン論理についての健全な証明系になっている. つま り, どちらでも実行がうまく終了すれば, 出てきた結果がプログラムを公理系 と解釈した場合の正しい定理になっているのである. このことは, プログラ ムの理論的解析などにとって便利な性質である.
一方, どちらも, 完全な証明系ではない. Prolog でも KL1 でもうまく証明 できない定理がある. カットや組込述語などの付加機能のない純粋な Prolog では, この不完全性は, 実行が終らないことがあるという形で現れる. KL1 では同様に実行が終らないことがあるのに加えて, 失敗という形で終ることも ある点が異なっている. このため, プログラム言語処理系をそのままホーン 論理の自動証明器としてみると, Prolog に比べて証明できる範囲がやや狭まっ ているわけだ. KL1 はその部分をあきらめることによって, 並列プログラム 言語として必要な機能を充実しているのである.