Математическая логика и теория алгоритмов

число».Т о г д а о б о з н а ч а е т ; «1 - четное число». Следовательно, формула ложна в этой интерпретации. Формула в этой интерпре­ тации представляет истинное высказывание: ЗА'(<а; - четное число»). Таким образом, для данной формулыЛ формулыЛ и неравносильны. § 9. Унификация Процесс унификации является основным в формальных преобразованиях, выполняемых при нахождении резольвент (для метода резолюций). Пусть задано множество дизъюнктов. Каждый дизъюнкт составлен из литералов. Пример. Пусть имеем следующее множество дизъюнктов: Дизъюнкт Дизъюнкт . к. S- I P f e / o ) , » ) } ' ' ' V ' Литерал Литерал Литерал Термы литерала могут быть переменными, постоянными или выражениями, состоящими из функциональных букв и термов. Например, для литерала Р(х, J{y), Ъ) имеем, что х - переменная, fy) - сложный терм, b - постоянная. Подстановочный частный случай литерала получается при подстановке в литералы термов вместо переменных. Пусть имеем ли­ терал P{x,fiy), b). Его частными случаями будут; Р, = P(z,y(>v), b), Р2 = Р{х,Ла),Ь), Рг = P(g(z),f{a), b), Р4 -• Р{с, fia), b) - константный частный случай литерала или атом, так как нет переменных. 107