Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Отметим, что если А не является противоречием, то может быть, что А не равносильна Ag. Например, пусть А=ЗсР(х). Тогда As=P(a). Построим интер­ претацию для этих формул: /= ({1,2}; {х - четное число }, {0} , {1}), т.е. область интерпретации !М={\,2}, Р(х) обозначает предикат <а - четное число» и а=\. Следовательно, As=P(\) обозначает: «1 - четное число» и форму­ ла As ложна в этой интерпретации. Формула А в этой интерпретации представ­ ляет истинное высказывание: Зх{«х - четное число»). Таким образом, формулы А vi. As неравносильны. В ряде случаев может оказаться, что Л и равносиль­ ны, но в общем случае - нет. § 8. Унификация Процесс унификации является основным в формальных преобразованиях, выполняемых при нахождении резольвент из дизъюнктов. Напомним, что дизъюнктом или клаузой в логике предикатов считается выражение вида D = Ь±2. • • (Ci v С2 v ... v C „), где Ci , \ <i <n - литера­ лы, a Xi, X2, Xk все переменные встречающиеся в Q, \ < i <п, т.е. дизъюнкт содержит только кванторы общности по всем своим свободным переменным. Повторяясь, отметим, что в дальнейшем будем записывать дизъюнкты в упро­ щенном виде, опуская все кванторы общности, но, зная, что они всегда есть. Таким образом, будем писать: D = Ci v С2 v ... v С„, где Ci , \ <i <п - литералы. Пример. Пусть имеем следующее множество дизъюнктов: дизъюнкт дизъюнкт S = {P(x,f(y), Ъ) vP(x,f(a), b), -^(c,f(a), b)} литерал литерал литерал Термы литерала могут быть переменными, постоянными или выражения­ ми, состоящими из функциональных букв и термов. Например, для литерала P(x,f(y), b) имеем, что х - переменная , - сложный терм, b - постоянная. Подстановочный частный случай литерала получается при подстановке в литералы термов вместо переменных. Пусть имеем литерал L=P(x, f(у), b). Его частными случаями будут: Li =P(z,f(w), b), L2 =P(x,f(a), b), 73