Подстановки и унификации

Содержание:

• Подстановка в дизъюнктор
• Унификация
• Универсальный унификатор системы дизъюнкторов
• О существовании универсального унификатора для системы дизъюнкторов
  • Доказательство:
  • Подстановка
• Множество рассогласований
• Алгоритм унификации

Рассмотрим метод резолюций в логике первого порядка. Относительно переменных в дизъюнктах будем предполагать, что они связаны кванторами общности, но сами кванторы писать не будем. Отсюда следует, что две одинаковые переменные в разных дизъюнктах можно считать различными.

Заметим, прежде всего, что в логике первого порядка правило резолюций в прежнем виде уже не годится. Действительно, множество дизъюнктов $S = {P(x), \neg P(a)}$ невыполнимо (так как предполагается, что переменная $x$ связана квантором общности). В то же время, если использовать правило резолюций для логики высказываний, то из $S$ пустого дизъюнкта не получить. Содержательно понятно, что именно в этом случае надо сделать. Поскольку дизъюнкт $P(x)$ можно прочитать “для любого $x$ истинно $P(x)$”, ясно, что $P(x)$ истинно будет и для $x = a$. Сделав подстановку $х = a$, получим множество дизъюнктов $S’= {P(a), \neg P(a)}$. Множества $S$ и $S’$ одновременно выполнимы или невыполнимы. Но из $S’$ пустой дизъюнкт с помощью прежнего правила резолюций выводится тривиальным образом. Этот пример подсказывает, что в логике первого порядка правило резолюций надо дополнить возможностью делать подстановку.

В любой формальной теореме для свободных переменных подразумевается квантор общности $\forall$.

Подстановка в дизъюнктор

Пусть есть формула $F{x_1; x_2; …; x_n}$. Соответствие (или таблица соответствия) $\sigma: (x_1 \rightarrow t_1; x_2 \rightarrow t_2; …; x_n \rightarrow t_n)$ называется подстановкой в некоторый дизъюнктор термов $t_i$ вместо символов $x_i$.

Результаты подстановок будем обозначать $\sigma(F_i)$.

Унификация

Подстановка $\sigma$ называется унификацией для данной системы , если результаты применения этой подстановки ко всем дизъюнкторам совпадают между собой, то есть выполнено равенство $\sigma(F_1)=\sigma(F_2)=…=\sigma(F_n)$.

Пример 1. Для системы ${f^0x_1f^1(x_2);x_3x_4x_5}$ подстановка $(x_3 \rightarrow f^0; x_4 \rightarrow x_2; x_5 \rightarrow f^1(x_2))$ является унификатором.

Пример 2. Система ${x_1f^1(x_1);x_2x_2}$ не унифицируема.

Универсальный унификатор системы дизъюнкторов

Унификатор $\tau$ называется универсальным в данной системе дизъюнкторов, если для любой подстановки $\sigma$ верно $\tau(F) = (\tau \circ \sigma)(F) = \tau(\sigma(F))$.

О существовании универсального унификатора для системы дизъюнкторов

Если система дизъюнкторов унифицируема, то для нее существует универсальный унификатор.

Доказательство:

$\forall a \forall b (a \in R \land a \geq 0 \land b \in R \land B \geq 0 \rightarrow \frac{a+b}{2} \geq \sqrt{ab})$

$\forall a \forall b (a \in R \land a \geq 0 \land b \in R \land B \geq 0 \rightarrow \frac{a+b}{2} \geq \sqrt{ab})$	Что и как делаем
$a \in R, a \geq 0, b \in R, b \geq 0$	Теорема дедукции
$\exists c \in R: a = c^2 \land c \geq 0\ \exists d \in R: b = d^2 \land d \geq 0$	Теорема о полноте. $\forall x \geq 0 \exists y \geq 0 y^2 = x$ подстановка[]
$c - d \in R$	Свойство $R$ как кольца. $\forall x, y \in R \rightarrow x -y \in R$ - подстановка
$(c - d) ^2 \geq 0$	$\forall x \in R \rightarrow x^2 \geq 0 $ подстановка
$c^2 - 2cd + d^2 \geq 0$
$\frac{c^2 + d^2}{2} = cd$	$\forall x \in R \rightarrow x^2 \geq 0 $ подстановка $\sqrt{x}\sqrt{y} = \sqrt{xy}$

Подстановка

Принято писать не так: $x_i \rightarrow t_i$, а вот так: $x_i

t_i$

Подстановка $\sigma$ это такой набор предметных переменных: $\sigma = {x_{i_1}

t_1, x_{i_2}

t_2 … x_{i_n}}$, где $x_{j_k} \neq t_k$

$\tau = {x_{j_1}

s_1, x_{j_2}

s_2 … x_{j_n}

s_m}$

$\sigma \circ \tau$

1. ${x_{i_1}

   t_1^{\sigma}

   x_{i_2}}$

2. вычеркиваем для $x_{j_k} = x_{i_l}$
3. вычеркиваем, если $r_k^{\sigma} = x_{j_k}$

$\sigma = {x_1

x_2 , x_2

f^2_1 x_1 x_3, x_3

f_1^0}$

$\tau = {x_1

f_1^1 , x_2, x_2

x_1, x_3

x_4, x_4

x_3}$

Множество рассогласований

Пусть $M$ - множество литералов(или термов)ю Выделим первую слева позицию, в которой не для всех литералов(или термов) стоит один и тот же символ. Затем в каждом литерале выпишем выражение, которое начинается символом, занимаюзим эту позицию. (Этими выражениями могут быть сам литерал, атомарная формула или терм.) Множество полученных выражений называется множеством рассогласований.

Например:

$M = {P(x, f(y), a), P(x, u, g(y)), P(x, c, v)}​$, то первая слева позиция, в которой не все литералы имеют один и тот же символ - пятая позиция. Множество рассогласований состоит из термов $f(y), u, c​$. Множество рассогласований ${P(x, y), \neg P(a, g(z))}​$ есть само множество. Если $M = {\neg P(x, y), \neg Q(a, v)}​$, то множество рассогласований равно ${P(x, y), Q(a, v)}​$.

Алгоритм унификации

1. Положить $k=0, M_k = M, \sigma_k = \epsilon$
2. Если множество $M_k$ состоит из одного литерала, то выдать $\sigma_k$ в качестве наиболее общего унификатора и завершить работу. В противном случае найти множество $N_k$ рассогласований $M_k$.
3. Если в множестве $N_k$ существует переменная $v_k$ и терм $t_k$ не содержащий $v_k$, то перейти к шагу 4, иначе выдать сообщение о том, что множество $M$ неунифицируемо и завершить работу.
4. Положить $\sigma_(k+1) = \sigma_k * {v_k = t_k}$ (подстановка $\sigma_(k+1))$ получается из $\sigma_k$ заменой $v_k$ на $t_k$ и, возможно, добавлением равенства $v_k = t_k$). В множестве $M_k$ выполнить замену $v_k = t_k$, полученное множество литералов взять в качестве $M_(k+1)$.
5. Положить $k = k+1$ и перейти к шагу 2.