Зарипова, Э.Р. Дискретная математика Часть II. Математическая логика

67 Определение. Подстановка – это конечное множество вида {t 1 | v 1 ,…,t n | v n } , где каждая v i – переменная, каждый t i – терм, отличный от v i , все v i различны. Пример 13.2. {f(z) | x,y | z}, {a | x,g(y) | y,f(g(b)) | z}. Определение. Пусть  ={t 1 | v 1 ,…,t n | v n } – подстановка и E – выражение. Тогда E  – выражение, полученное из E заменой одновременно всех вхождений переменной v i , i 1 n ,  в E на терм t i . E  называют примером E . Пример 13.3.  ={a | x, f(b) | y, c | z}, E=P(x,y,z), E  = P(a, f(b), c). Определение. Пусть  = {t 1 | x 1 ,…,t n | x n } и  = {u 1 | y 1 ,…,u m | y m } – две подстановки. Тогда композиция  и  (обозначается  ) есть подстановка, которая получается из множества {t 1  | x 1 ,…,t n  | x n , u 1 | y 1 ,…,u m | y m } вычеркиванием всех элементов t j  /x j , для которых t j  =x j и всех элементов u i | y i таких, что y i  {x 1 ,…,x n } . Пример 13.4.  ={t 1 | x 1 , t 2 | x 2 }={f(y) | x, z | y}  = {u 1 | y 1 , u 2 | y 2 , u 3 | y 3 }= {a | x, b | y, y | z} Тогда {t 1  | x 1 , t 2  | x 2 , u 1 | y 1 , u 2 | y 2 , u 3 | y 3 }={f(b) | x, y | y, a | x, b | y, y | z}. Однако, т.к. t 2  =x 2 , то t 2  | x 2 (т.е. y | y ) необходимо вычеркнуть. Также нужно вычеркнуть u 1 | y 1 и u 2 /y 2 , т.к. y 1 и y 2  {x 1 ,x 2 } . Таким образом получаем  = {f(b) | x, y | z}. Определение. Подстановка  называется унификатором для множества {E 1 ,…,E k } тогда и только тогда, когда E 1  = … = E k  .