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

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

Если в формулу $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\}^n_{i=1}$

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

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

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

Набор формул $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\}^n_{i=1} \land C = B(\dots,x_i,\dots)\{X_i//x_i\}^n_{i=1}$

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

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

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

См. также

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