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

Частный случай формулПравить

Если в формулу   вместо переменных   подставить соответственно формулы   то получится формула  , которая называется частным случаем формулы  :

 

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

Набор подстановок   называется унификатором.

Частный случай набора формулПравить

Набор формул   называется частным случаем набора формул  , если каждая формула   является частным случаем формулы   при одном и том же наборе подстановок.

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

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

 

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

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

Набор формул   называется совместным частным случаем наборов формул   и  , если каждая формула   является частным случаем формул   и   при одном и том же наборе подстановок.

Задача унификацииПравить

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

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

См. такжеПравить