Частный случай формулы
Частный случай формул
правитьЕсли в формулу вместо переменных подставить соответственно формулы то получится формула , которая называется частным случаем формулы :
Каждая формула подставляется вместо всех вхождений переменной .
Набор подстановок называется унификатором.
Частный случай набора формул
правитьНабор формул называется частным случаем набора формул , если каждая формула является частным случаем формулы при одном и том же наборе подстановок.
Совместный частный случай формул
правитьФормула называется совместным частным случаем формул и , если является частным случаем формулы и одновременно частным случаем формулы при одном и том же наборе подстановок, то есть
Формулы, которые имеют совместный частный случай, называются унифицируемыми, а набор подстановок , с помощью которого получается совместный частный случай унифицируемых формул, называется общим унификатором.
Совместный частный случай набора формул
правитьНабор формул называется совместным частным случаем наборов формул и , если каждая формула является частным случаем формул и при одном и том же наборе подстановок.
Задача унификации
правитьЗадача унификации — определить, являются ли две формулы частным случаем одной и той же, в частности, друг друга.
Задача алгоритмически неразрешима в общем случае, если используются термы высших порядков (то есть знаки функций).
См. также
правитьЭто заготовка статьи по математике. Помогите Википедии, дополнив её. |
Это заготовка статьи по логике. Помогите Википедии, дополнив её. |
В статье не хватает ссылок на источники (см. рекомендации по поиску). |