Частный случай формулы

Частный случай формул

Если в формулу $A(x_1,\dots ,x_n)$ вместо переменных $x_1,\dots ,x_n$ подставить соответственно формулы $B_1,\dots ,B_n$ то получится формула $B$, которая называется частным случаем формулы $A$:

$B=A(\dots ,x_i,\dots )\{B_i//x_i{\}}_{i=1}^n$

Каждая формула $B_i$ подставляется вместо всех вхождений переменной $x_i$.

Набор подстановок $\{B_i//x_i{\}}_{i=1}^n$ называется унификатором.

Частный случай набора формул

Набор формул $B_1,\dots ,B_n$ называется частным случаем набора формул $A_1,\dots ,A_n$, если каждая формула $B_i$ является частным случаем формулы $A_i$ при одном и том же наборе подстановок.

Совместный частный случай формул

Формула $C$ называется совместным частным случаем формул $A$ и $B$, если $C$ является частным случаем формулы $A$ и одновременно частным случаем формулы $B$ при одном и том же наборе подстановок, то есть

$C=A(\dots ,x_i,\dots )\{X_i//x_i{\}}_{i=1}^n\wedge C=B(\dots ,x_i,\dots )\{X_i//x_i{\}}_{i=1}^n$

Формулы, которые имеют совместный частный случай, называются унифицируемыми, а набор подстановок $\{X_i//x_i{\}}_{i=1}^n$, с помощью которого получается совместный частный случай унифицируемых формул, называется общим унификатором.

Совместный частный случай набора формул

Набор формул $C_1,\dots ,C_n$ называется совместным частным случаем наборов формул $A_1,\dots ,A_n$ и $B_1,\dots ,B_n$, если каждая формула $C_i$ является частным случаем формул $A_i$ и $B_i$ при одном и том же наборе подстановок.

Задача унификации

Задача унификации — определить, являются ли две формулы частным случаем одной и той же, в частности, друг друга.

Задача алгоритмически неразрешима в общем случае, если используются термы высших порядков (то есть знаки функций).

См. также

• Частный случай (логика)