Подстановки и унификации
Содержание:
- Подстановка в дизъюнктор
- Унификация
- Универсальный унификатор системы дизъюнкторов
- О существовании универсального унификатора для системы дизъюнкторов
- Множество рассогласований
- Алгоритм унификации
Рассмотрим метод резолюций в логике первого порядка. Относительно переменных в дизъюнктах будем предполагать, что они связаны кванторами общности, но сами кванторы писать не будем. Отсюда следует, что две одинаковые переменные в разных дизъюнктах можно считать различными.
Заметим, прежде всего, что в логике первого порядка правило резолюций в прежнем виде уже не годится. Действительно, множество дизъюнктов $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$
-
${x_{i_1} t_1^{\sigma} x_{i_2}}$ - вычеркиваем для $x_{j_k} = x_{i_l}$
- вычеркиваем, если $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)}$.
Алгоритм унификации
- Положить $k=0, M_k = M, \sigma_k = \epsilon$
- Если множество $M_k$ состоит из одного литерала, то выдать $\sigma_k$ в качестве наиболее общего унификатора и завершить работу. В противном случае найти множество $N_k$ рассогласований $M_k$.
- Если в множестве $N_k$ существует переменная $v_k$ и терм $t_k$ не содержащий $v_k$, то перейти к шагу 4, иначе выдать сообщение о том, что множество $M$ неунифицируемо и завершить работу.
- Положить $\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)$.
- Положить $k = k+1$ и перейти к шагу 2.