Логическое программирование на языке Visual Prolog. Солдатова О.П - 8 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

8
Тем не менее, существуют алгоритмы поиска доказательства, которые
могут подтвердить, что формула общезначима, если она на самом деле
общезначима (для необщезначимых формул эти алгоритмы, вообще говоря,
не заканчивают свою работу).
Очень важный подход к автоматическому доказательству теорем был
дан Эрбраном в 1930 году. По определению общезначимая формула есть
формула, которая истинна
при всех интерпретациях. Эрбран разработал
алгоритм нахождения интерпретации, которая опровергает данную формулу.
Однако, если данная формула действительно общезначима, то никакой
интерпретации не существует и алгоритм заканчивает работу за конечное
число шагов. Метод Эрбрана служит основой для большинства современных
автоматических алгоритмов поиска доказательства.
Гилмор в 1959 году одним из первых реализовал процедуру
Эрбрана.
Его программа была предназначена для обнаружения противоречивости
отрицания данной формулы, так как формула общезначима тогда и только
тогда, когда ее отрицание противоречиво. Однако программа Гилмора
оказалась неэффективной и в 1960 году метод Гилмора был улучшен
Девисом и Патнемом. Но их улучшение оказалось недостаточным, так как
многие общезначимые формулы логики предикатов все
еще не могли быть
доказаны на ЭВМ за разумное время.
Главный шаг вперед сделал Робинсон в 1965 году, который ввел так
называемый метод резолюций, который оказался много эффективней, чем
любая описанная ранее процедура. После введения метода резолюций был
предложен ряд стратегий для увеличения его эффективности. Такими
стратегиями являются семантическая резолюция, лок-
резолюция, линейная
резолюция, стратегия предпочтения единичных и стратегия поддержки.
1.2.2 Скулемовские стандартные формы.
Процедуры доказательства по Эрбрану или методу резолюций на
самом деле являются процедурами опровержения, то есть вместо
доказательства общезначимости формулы доказывается, что ее отрицание
противоречиво. Кроме того, эти процедуры опровержения применяются к
некоторой стандартной форме, которая была введена Девисом
и Патнемом.
По существу они использовали следующие идеи:
1. Формула логики предикатов может быть сведена к ПНФ, в которой
матрица не содержит никаких кванторов, а префикс есть
последовательность кванторов.
2. Поскольку матрица не содержит кванторов, она может быть сведена
к конъюнктивной нормальной форме.
3. Сохраняя противоречивость формулы, в ней можно исключить
кванторы существования путем использования скулемовских
функций.

Страницы