Page 43 - 6109

узагальнення). В той же час за попереднім правило отримати пустий диз’юнкт
із S неможливо. Оскільки диз’юнкт Р(х) можна розуміти так, що Р(х) істинно
для будь-якого х, то Р(х) буде істинним і для х = а. Отже зробивши підстановку,
отримаємо множину диз’юнктів S’={P(а), ~P(а)}. Множини S та S’ одночасно
не виконувані, але з S’ можна вивести пустий диз’юнкт. Таким чином, в логіці
предикатів правило резолюцій необхідно доповнити можливістю робити
підстановки.
Підстановкою називається множина рівностей  = {x 1 = t 1, x 2 = t 2,…,
x n = t n}, де x 1, x 1, x n – різні змінні, t 1, t 2,…, t n – терми, причому терм t і не містить
змінної х і.
Якщо ={x 1=t 1, x 2=t 2,…, x n=t n} – підстановка, а F – диз’юнкт, то через
(F) будемо позначати диз’юнкт, що отримується з М, одночасною заміною x 1
на t 1, x 2 на t 2,…, x n на t n. Причому терми можуть підставлятися лише замість
змінних, а не констант.
Підстановка σ називається уніфікатором для множини виразів {F 1, ...,
F п}, якщо σ(F 1)= σ(F 2) = ... = σ(F n). Якщо множина уніфікована, то існує як
правило не один уніфікатор множини, а декілька, серед яких виділяється
найбільш загальний уніфікатор.

Уніфікатор σ для множини виразів {F 1,..., F п} називається найбільш
загальним уніфікатором, якщо для будь-якого уніфікатора θ цієї множини
існує така підстановка λ, що θ являтиме собою композицію підстановок σ і λ (θ=
σ λ).
Композицією підстановок  = {x 1 = t 1, x 2 = t 2,…, x n = t n} і λ = {у 1 = u 1,
у 2 = u 2,…, у m = u m} називається підстановка θ ={x 1 = λ(t 1), x 2 = λ(t 2),…, x n = λ(t n),
у 1=u 1, у 2=u 2,…, у m=u m}, з якої викреслені всі рівності виду x i=x i та у і=u і, у і  {х 1,
..., х п}.
Наприклад, (Приклад 2)
 = {x = f(y), z = y, u = g(d)}
 = {x = c, y = z}
  = { x = f(y), z = z, u = g(d), x = c, y = z } = { x = f(y), u = g(d), y = z }
Тепер можна сформулювати загальне правило резолюцій.
Дві фрази, що містять контрарну пару, можуть бути резольвовані одна з
іншою, якщо літерали, що входять до контрарної пари, можуть бути
уніфіковані, тобто якщо для них існує найбільш загальний уніфікатор σ.
Результатом резолюції є диз'юнкція літералів, які залишаються в обох фразах
після викреслення контрарної пари, причому до цих літералів повинен бути
застосований уніфікатор σ.
В логіці предикатів також вводиться правило зклейки. Із дизюнкту

P(t 1,…, t n)… P(s 1,…, s n)  F виводимо дизюнкт (P(t 1,…, t n))  (F)
(склейка першого дизюнкта).
  знак заперечення або його відсутність.
Наприклад,
~P(x, y) ~P(y, x)  ~P(a, a)  Q(x, y, v)  ~P(a, a)  Q(a, a, v)
Тоді виводом із множини дизюнктів S називається послідовність
диз’юнктів D 1, D 2, …,D n така, що кожний диз’юнкт D j цієї послідовності

43