Поиск общей разрешающей процедуры для проверки общезначимости формул начал Лейбниц в XVII веке, затем был продолжен в начале XX века до тех пор, пока в 1936 году Черч и Тьюринг независимо не доказали, что не существует никакой общей разрешающей процедуры, никакого алгоритма, проверяющего общезначимость формул в логике предикатов первого порядка.
Тем не менее, существуют алгоритмы поиска доказательства, которые могут подтвердить, что формула общезначима, если она на самом деле общезначима (для необщезначимых формул эти алгоритмы, вообще говоря, не заканчивают свою работу).
Очень важный подход к автоматическому доказательству теорем был дан Эрбраном в 1930 году. По определению общезначимая формула есть формула, которая истинна при всех интерпретациях. Эрбран разработал алгоритм нахождения интерпретации, которая опровергает данную формулу. Однако, если данная формула действительно общезначима, то никакой интерпретации не существует и алгоритм заканчивает работу за конечное число шагов. Метод Эрбрана служит основой для большинства современных автоматических алгоритмов поиска доказательства.
Гилмор в 1959 году одним из первых реализовал процедуру Эрбрана. Его программа была предназначена для обнаружения противоречивости отрицания данной формулы, так как формула общезначима тогда и только тогда, когда ее отрицание противоречиво. Однако, программа Гилмора оказалась неэффективной и в 1960 году метод Гилмора был улучшен Девисом и Патнемом. Однако их улучшение оказалось недостаточным, так как многие общезначимые формулы логики предикатов все еще не могли быть доказаны на ЭВМ за разумное время.
Главный шаг вперед сделал Робинсон в 1965 году, который ввел так называемый метод резолюций, который оказался много эффективней, чем любая описанная ранее процедура. После введения метода резолюций был предложен ряд стратегий для увеличения его эффективности. Такими стратегиями являются семантическая резолюция, лок-резолюция, линейная резолюция, стратегия предпочтения единичных и стратегия поддержки.
Процедуры доказательства по Эрбрану или методу резолюций на самом деле являются процедурами опровержения, то есть вместо доказательства общезначимости формулы доказывается, что ее отрицание противоречиво. Кроме того, эти процедуры опровержения применяются к некоторой стандартной форме, которая была введена Девисом и Патнемом. По существу они использовали следующие идеи:
1. Формула логики предикатов может быть сведена к ПНФ, в которой матрица не содержит никаких кванторов, а префикс есть последовательность кванторов.
2. Поскольку матрица не содержит кванторов, она может быть сведена к конъюнктивной нормальной форме.
3. Сохраняя противоречивость формулы, в ней можно исключить кванторы существования путем использования скулемовских функций.
Алгоритм преобразования формулы в ПНФ известен. При помощи законов эквивалентных преобразований логики высказываний можно свести матрицу к КНФ.
Алгоритм преобразования формул в ДНФ и КНФ.
Шаг 1. Используем законы законы 1 и 2 исчисления высказываний для того, чтобы исключить логические связки импликации и эквивалентности.
Шаг 2. Многократно используем закон двойного отрицания, и законы де Моргана, чтобы внести знак отрицания внутрь формулы.
Шаг 3. Несколько раз используем дистрибутивные законы и другие законы, чтобы получить НФ.
Алгоритм преобразования формулы (K1x1)…(Knxn) (M), где каждое (Kixi), i = 1,…,n, есть или ("xi) или ($xi), и M есть КНФ в скулемовскую нормальную форму (СНФ) приведен ниже.
Алгоритм преобразования ПНФ в ССФ.
Шаг 1. Представим формулу в ПНФ (K1x1)…(Knxn) (M), где M есть КНФ. Пусть Kr есть квантор существования в префиксе (K1x1)…(Knxn), 1<=r<=n.
Шаг 2. Если никакой квантор всеобщности не стоит левее Kr– выберем новую константу c, отличную от других констант, входящих в M, заменим все xrв M на c и вычеркнем Krxr из префикса. Если K1,…Ki– список всех кванторов всеобщности, встречающихся в префиксе левее Kr, 1< i<r, выберем новый i –местный функциональный символ f, отличный от других функциональных символов, заменим все xrв M на f(x1, x2,…xi) и вычеркнем Krxr из префикса.
Шаг 3. Применим шаг 2 для всех кванторов существования в префиксе. Последняя из полученных формул есть скулемовская стандартная форма формулы. Константы и функции, используемые для замены переменных квантора существования, называются скулемовскими функциями.
Пример 8. Получить ССФ для формулы ($x)("y)("z)($u)("v)($w) (P(x, y, z, u, v, w).
В этой формуле левее ($x) нет никаких кванторов всеобщности, левее ($u) стоят ("y) и ("z), а левее ($w) стоят ("y), ("z) и ("v). Следовательно, мы заменим переменную x на константу a, переменную u - на двухместную f(y, z), переменную w - на трехместную функцию g(y, z, v). Таким образом, мы получаем следующую стандартную форму написанной выше формулы:
("y)("z)("v)(P(a, y, z, f(y, z), g(y, z, v)).
Определение 22: Дизъюнктом называется дизъюнкция литералов. Дизъюнкт, содержащий r литералов, называется r- литеральным дизъюнктом. Однолитеральный дизъюнкт называется единичным дизъюнктом. Если дизъюнкт не содержит никаких литералов, то он называется пустым дизъюнктом- я . Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинными при любых интерпретациях, то пустой дизъюнкт всегда ложен.
Определение 23: Множество дизъюнктов S есть конъюнкция всех дизъюнктов из S , где каждая переменная в S считается управляемой квантором всеобщности.
Вследствие последнего определения, ССФ может быть представлена множеством дизъюнктов.
Пример 9. Получить скулемовскую стандартную форму формулы
("x) (P(x) Ù ("y)(Ø ("z)Q(z, y)® ($u)R(u, y))) и представить её в виде множества дизъюнктов.
((Ø P(x, y) Ú R(x, y, z ))Ù (Q(x, z) Ú R(x, y, z)) Ù (Ø Q(x, z) Ù P(x, y))).
Затем избавимся от кванторов существования в префиксе:
Так как перед ($y)($z) есть ("x), то переменные y, z заменяются соответственно одноместными функциями f(x), g(x). Таким образом, мы получаем следующую стандартную форму:
Теорема 3. Пусть S – множество дизъюнктов, которые представляют ССФ формулы F. Тогда F противоречива в том и только в том случае, когда S противоречиво.
На основании теорем 2 и 3 можно сделать вывод, что формула G является логическим следствием формулы F тогда, когда противоречива конъюнкция множества S и формулы ШG, то есть противоречива формула S1 Щ S2 Щ …Sn Щ ШG. Таким образом, если в множество S добавить негативный литерал ШG и доказать, что полученное множество противоречиво, то тем самым можно доказать выводимость G из множества S.
