Унификация – это алгоритм определения необходимых подстановок с целью приведения в соответствие 2х выражений исчисления предикатов.
[ Пример: Все люди смертны. Сократ человек, поэтому он смертен. 
человек(Сократ). Заменив Х на Сократ, получим Х человек(Сократ) ->смертный(Сократ). Терм «Сократ» был использован в качестве подстановки для Х в выражение . Эта подстановка позволяла применить правило modus ponens и получить вывод смертный(Сократ).]
Унификация позволяет делать выводы на множество логических утверждений. Для этого логическая БД должна быть выражена в соответствующей форме. Один из аспектов формы – все переменные под знаком квантора всеобщности. Переменные, стоящие под знаком квантора существования, можно устранить из предложений БД, заменив константами, обеспечивающими истинность предложения.
[ Пример: 
может быть заменено родитель(Боб,Том).]
Процесс удаления переменных, связанных квантором существования, усложнен фактом, что значения этих подстановок могут зависеть от значения других переменных в выражении.
Сколемизация – замена каждой переменной, связанной квантором существования, функцией нескольких или всех имеющихся в предложении переменных, которые возвращают соответствующую константу.
Дата добавления: 2015-07-10; просмотров: 197 | Нарушение авторских прав