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

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

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

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

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

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

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

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

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

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

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

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}

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

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

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

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