Русская Википедия:Частный случай формулы

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

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

Если в формулу <math>A(x_1,\dots,x_n)</math> вместо переменных <math>x_1,\dots,x_n</math> подставить соответственно формулы <math>B_1,\dots,B_n</math> то получится формула <math>B</math>, которая называется частным случаем формулы <math>A</math>:

<math>B = A(\dots,x_i,\dots)\{B_i//x_i\}^n_{i=1}</math>

Каждая формула <math>B_i</math> подставляется вместо всех вхождений переменной <math>x_i</math>.

Набор подстановок <math>\{B_i//x_i\}^n_{i=1}</math> называется унификатором.

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

Набор формул <math>B_1,\dots,B_n</math> называется частным случаем набора формул <math>A_1,\dots,A_n</math>, если каждая формула <math>B_i</math> является частным случаем формулы <math>A_i</math> при одном и том же наборе подстановок.

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

Формула <math>C</math> называется совместным частным случаем формул <math>A</math> и <math>B</math>, если <math>C</math> является частным случаем формулы <math>A</math> и одновременно частным случаем формулы <math>B</math> при одном и том же наборе подстановок, то есть

<math>C = A(\dots,x_i,\dots)\{X_i//x_i\}^n_{i=1} \land C = B(\dots,x_i,\dots)\{X_i//x_i\}^n_{i=1}</math>

Формулы, которые имеют совместный частный случай, называются унифицируемыми, а набор подстановок <math>\{X_i//x_i\}^n_{i=1}</math>, с помощью которого получается совместный частный случай унифицируемых формул, называется общим унификатором.

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

Набор формул <math>C_1,\dots,C_n</math> называется совместным частным случаем наборов формул <math>A_1,\dots,A_n</math> и <math>B_1,\dots,B_n</math>, если каждая формула <math>C_i</math> является частным случаем формул <math>A_i</math> и <math>B_i</math> при одном и том же наборе подстановок.

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

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

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

См. также

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