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

Если в формулу ${\displaystyle A(x_{1},\dots ,x_{n})}$ вместо переменных ${\displaystyle x_{1},\dots ,x_{n}}$ подставить соответственно формулы ${\displaystyle B_{1},\dots ,B_{n}}$ то получится формула ${\displaystyle B}$, которая называется частным случаем формулы ${\displaystyle A}$:

${\displaystyle B=A(\dots ,x_{i},\dots )\{B_{i}//x_{i}\}_{i=1}^{n}}$

Каждая формула ${\displaystyle B_{i}}$ подставляется вместо всех вхождений переменной ${\displaystyle x_{i}}$.

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

Набор формул ${\displaystyle B_{1},\dots ,B_{n}}$ называется частным случаем набора формул ${\displaystyle A_{1},\dots ,A_{n}}$, если каждая формула ${\displaystyle B_{i}}$ является частным случаем формулы ${\displaystyle A_{i}}$ при одном и том же наборе подстановок.

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

${\displaystyle 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}}$

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

Набор формул ${\displaystyle C_{1},\dots ,C_{n}}$ называется совместным частным случаем наборов формул ${\displaystyle A_{1},\dots ,A_{n}}$ и ${\displaystyle B_{1},\dots ,B_{n}}$, если каждая формула ${\displaystyle C_{i}}$ является частным случаем формул ${\displaystyle A_{i}}$ и ${\displaystyle B_{i}}$ при одном и том же наборе подстановок.

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

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

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