平成26年度 秋期 午前Ⅱ 問11

✓ これが正解エユニフィケーション

解説

論理型言語では、ユニフィケーションで項を照合して証明を進めます。

論理型プログラミングでは、事実と規則を論理式として記述し、問い合わせとして与えた命題が成り立つかを、処理系が推論によって証明します。その推論の中で、二つの項に含まれる変数に値を当てはめて両者を一致させる操作がユニフィケーション（単一化）です。証明したい目標と規則の頭部をユニフィケーションで結び付け、成り立つまで探索を進めます。見分ける軸は、論理型の操作か、それ以外の考え方の操作かです。ほかの三つはオブジェクト指向などで使われるメソッドやメッセージの用語なので、パラダイムの違いに目を向ければ選べます。

ほかの選択肢はなぜ違うのか

• アオーバライド：オーバライドは、スーパクラスで定義されたメソッドをサブクラスで定義し直すことです。継承を使うオブジェクト指向の仕組みであり、論理型で命題を証明するための操作ではありません。
• イオーバロード：オーバロードは、同じ名前のメソッドや関数を、引数の型や数を変えて複数定義することです。呼出しのときに引数で使い分ける仕組みで、命題の証明を進める操作とは関係がありません。
• ウメッセージパッシング：メッセージパッシングは、オブジェクトどうしがメッセージを送り合って処理を依頼する仕組みです。オブジェクト指向の計算の進め方を表す言葉であり、論理型の証明の基本操作ではありません。