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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Частный случай формул[править | править вики-текст]

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

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

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

Частный случай набора формул[править | править вики-текст]

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

Совместный частный случай формул[править | править вики-текст]

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

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

Совместный частный случай набора формул[править | править вики-текст]

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

Задача унификации[править | править вики-текст]

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

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

См. также[править | править вики-текст]