令和6年度 春期 午前Ⅱ 問9

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

解説

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

論理型プログラミングでは、事実と規則を論理式として書いておき、問い合わせた命題が成り立つかを処理系が証明しようとします。そのときの基本操作がユニフィケーションで、二つの項を比べ、変数に適切な値を当てはめて同じ形にできるかを調べます。同じ形にできれば、その当てはめを手がかりに規則をたどり、証明を先へ進めます。設問の、命題の証明を行うための基本的な機能という記述は、この照合の働きを指しています。ほかの選択肢は、メソッドの再定義や多重定義、オブジェクト間の通信といったオブジェクト指向の用語です。論理型は照合して当てはめる、オブジェクト指向はメソッドを定義して呼ぶ、と系統で分けると区別できます。

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

• アオーバーライド：オーバーライドは、スーパークラスで定義されたメソッドをサブクラスで定義し直すことです。オブジェクト指向での継承に伴う仕組みであり、論理式を照合して命題を証明する働きはもちません。
• イオーバーロード：オーバーロードは、同じ名前で引数の型や数が異なるメソッドを複数定義できる仕組みです。呼出し時にどれを使うかが引数で決まるだけで、命題の証明を進める基本機能とは関係しません。
• ウメッセージパッシング：メッセージパッシングは、オブジェクトどうしがメッセージを送り合って処理を依頼する仕組みです。オブジェクト指向の協調の仕方を表す言葉で、論理型での証明の手段ではありません。