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

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

Если в формулу $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}\land 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}$ при одном и том же наборе подстановок.

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

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

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

См. также

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