Логическое и функциональное программирование (стр. 14 из 16)
("x)($y)("z)($w)F(x ,y ,z, w) = ("x)("z)F(x, f(x), z, g(x, z)).
Если подобным образом исключить связанные квантором существования переменные, то любые другие переменные будут связаны только квантором общности и не надо пояснять, что преременные связаны этим квантором. Следовательно, квантор общности можно исключить. Для примера получим:
Такое представление и есть сколемовская нормальная форма.
Теперь можем определить алгоритм получения сколемовской формы:
1. Составить список Lпеременных, связанных квантором общности. Сначала список Lпуст.
2. Пусть Ci– рассматриваемое предложение, j– номер использующейся сколемовской функции Sij. Положим j = 1.
3. Удалить кванторы , начиная с самого левого и применяя в зависимости от необходимости правила а или б.
а. Если рассматривается квантор "x, то удалить его и добавить x к списку L.
б. Если рассматривается квантор $x, то удалить его и заменить x во всем предложении Ci термом Sij(x1, …, xk), где x1, …, xk переменные, находящиеся в этот момент в списке L. Увеличить j на 1.
Следующим шагом является переход к конъюнктивной нормальной форме, а затем к клаузальной форме, то есть форме предложений.
Приведение к конъюнктивной нормальной форме осуществляется заменой пока это возможно (AÙB)ÚCна (AÚC)Ù(BÚC). В результате получим выражения вида A1Ù … ÙAn, где Aiимеет вид (
, причем 
есть терм или атомарный предикат или атомарная формула или их отрицание. Целесообразно осуществить и минимизацию по следующим правилам: 
Наконец, исключаем связку Ù, заменяя AÙB на две формулы A, B. В результате многократной замены получим множество формул, каждая из которых является предложением. Это и есть клаузальная нормальная форма.
4.2.2.3 Предложения Хорна
Все клаузальные формулы (предложения) представляют собой несколько предикатов, то есть:
Эти формулы в зависимости от k, l классифицируются по нескольким типам.
(1) Тип 1: k = 0, l = 1.
Предложение представляет собой единичный предикат, и оно может быть записано как ®F(t1, t2, …, tm), где t1, t2, …, tm– термы. В случае когда все термы представляют собой константы, они описывают факты, которые соответствуют данным из БД. Если термы содержат переменные, то они задают общезначимые представления, высказываемые для группы фактов. Например, таким представлением является:
® текучесть(x): все течет, все изменяется.
(2) Тип 2: k³1, l = 0.
Этот тип можно записать в виде:
F1ÙF2Ù…ÙFk®.
Обычно используется для описания вопроса. Причина, по которой данный тип предложения представляется вопросом, является то, что ответ на вопрос реализуется в виде процедуры доказательства, однако для этого доказательства используется метод опровержения, при котором создается отрицание вопроса и доказывается, что отрицание не выполняется.
(3) Тип : k³1, l=1.
Этот тип соответствует записи в форме «Если ___, то ____.».
F1ÙF2Ù…ÙFk®G1.
(4) Тип: k=0, l>1.
Этот тип имеет вид:
®G1ÚG2Ú…ÚGl
и используется при представлении информации, содержащей нечеткость. Обычно нечеткость возникает при неполноте информации. В этой формуле появляется неполнота информации в том смысле, что из нее нельзя определить, какой из предикатов G1, …, Gl является истиной.
(5) Тип: k³1, l>1.
Это наиболее общий тип.
В системе предложений Хорна среди всех перечисленных типов предложений допустимы типы предложений 1, 2, 3, а 4, 5 запрещены.
4.2.3Формализация процесса доказательств
Доказательство демонстрирует, что некоторая ППФ является теоремой на заданном множестве аксиом S (то есть результатом логического вывода из аксиом).
Положим, что S есть множество из n ППФ, а именно, A1, A2, …, An, и пусть ППФ, для которой требуется вычислить является ли она теоремой, есть B. В таких случаях можно сказать, что доказательство показывает истинность ППФ вида:
(A1Ù…ÙAn®B) (1)
при любой его интерпретации. Можно сказать по другому: это определение эквивалентно тому, что отрицание формулы:
(2)не выполняется (ложно) при любой интерпретации.
Поскольку эта формула является ППФ, то ее можно преобразовать к клаузальной форме, используя для этого приведенный выше алгоритм. Пусть преобразованная ППФ есть S.
Основная идея метода, называемого методом резолюции, состоит:
1. В проверке содержит или не содержит S пустое предложение.
2. В проверке выводится или не выводится пустое предложение из S, если пустое предложение в S отсутствует.
Любое предложение Ci, из которого образуется S, является совокупностью атомарных предикатов или их отрицаний (предикат и его отрицание называются литералами), соединенных символами дизъюнкции, вида:
Сама же S является конъюнктивной формой, то есть имеет вид:
Следовательно, условием истинности S является условие истинности всех Ci в совокупности.
Условием ложности S является ложность по крайней мере одного Ci. Однако, условием, что Ciбудет ложным в какой-нибудь интерпретации, является то, что множество
будет пустым. Это легко показать. Положим, что это не так, тогда среди всех возможных интерпретаций имеется такая, что какой-нибудь из литералов этого множества или все они будут истиной и тогда Ciне будет ложью. Следовательно, если S содержит пустые предложения, формула (2) является ложью, а это показывает, что B выводится из группы предикатов A1, … , An, то есть из S.4.2.3.1 Метод резолюций для логики высказываний
Предикат, который не содержит переменных, совпадает с высказыванием. Для упрощения рассмотрим сначала резолюцию для высказываний.
Предположим, что в множестве предложений есть дополнительные литералы (которые отличаются только символами отрицания Lи 
) вида:
Исключим из этих двух предложений дополнительные литералы и представим оставшуюся часть в дизъюнктивной форме (такое представление называется резольвентой):
После проведения этой операции легко видеть, что Cявляется логическим заключением Ci и Cj. Следовательно, добавление C к множеству Sне влияет на вывод об истинности или ложности S. Если выполняется Ci = L, 
то Cпусто. То что C является логическим заключением из Sи C пусто, указывает на ложность исходной логической формулы.
Приведем простой пример такого доказательства:
Получим доказательство принципом резолюции:
- пустое предложение.Такой вывод теорем из аксиоматической системы носит название дедукции. Алгоритм дедуктивного вывода удобно представлять с помощью древовидной структуры:
Такая структура называется дедуктивным деревом или деревом вывода.
4.2.3.2 Принцип резолюции для логики предикатов
Поскольку в логике предикатов внутри предикатов содержатся переменные, то алгоритм доказательства несколько изменяется. В этом случае, перед тем как применить описанный алгоритм, будет проведена некоторая подстановка в переменные и вводится понятие унификации с помощью этой подстановки. Унификацию проиллюстрируем следующим простым примером.
Рассмотрим два предиката – L(x) и L(a). Предположим, что x– переменная, a- константа. В этих предикатах предикатные символы одинаковы, чего нельзя сказать о самих предикатах. Тем не менее подстановкой aв xодинаковыми (эта подстановка и называется унификацией).