yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Математика і інформатика->Содержание->Глава 5. АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМ

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

Глава 5. АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМ

5.1. Введение

Поиск общей разрешающей процедуры для проверки общезначимости формулы начат давно. Первым пытался найти такую процедуру Лейбниц (1646 - 1716), в дальнейшем над этим работала школа Гильберта. Это продолжалось до тех пор, пока Черч и Тьюринг независимо друг от друга не 'Казали, что не существует никакой общей разрешающей процедуры, какого алгоритма, проверяющего общезначимость формул в логике  первого порядка. Тем не менее существуют алгоритмы поиска доказательства, которые могут подтвердить, что формула общезначима. Для не общезначимых формул эти алгоритмы, вообще говоря, не заканчивают свою работу. Принимая во внимание результат Черча и Тьюринга, это лучшее, что мы можем ожидать от алгоритма поиска доказательства.

Очень важный подход к автоматическому доказательству теорем был дан Эрбраном в 1930г. По определению, общезначимая формула есть формула, которая истинна при всех интерпретациях. Эрбран разработал алгоритм нахождения интерпретации, которая опровергает данную формулу. Однако, если данная формула на самом деле общезначима, то такой интерпретации не существует и алгоритм оканчивает работу за конечное число шагов. Метод Эрбрана служит основой для большинства современных автоматических алгоритмов поиска доказательства.

Главный результат был получен Робинсоном, который ввел так называемый метод резолюций.

Процедуры поиска доказательства по Эрбрану или методу резолюций являются процедурами поиска опровержения, т. е. вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво. Эти процедуры опровержения применяются к "стандартной форме". Метод резолюций заключается в следующем.

•    Формула логики первого порядка может быть сведена к предваренной нормальной форме, в которой матрица не содержит никаких кванторов, а' префикс1 есть последовательности кванторов.

•     Поскольку матрица не содержит кванторов, она может быть сведена к конъюнктивной нормальной форме.

• Сохраняя противоречивость формулы, в ней можно элиминировать кванторы существования путем использования скулемовских функций.

 

31