Глава 13.

АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМ

13.1. Введение

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

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

В основе метода резолюций лежит процедура поиска опровер­жения, т.е. вместо доказательства общезначимости формулы дока­зывается, что отрицание формулы противоречиво. Метод опровер­жения для доказательства логического следования заключается в следующем. Пусть выполняется логическое следование: F1, F2 |= G. Тогда |= F1&F2G логически общезначима, и, следовательно, |(F1F2G)|=|F1F2G|F. Поскольку по определению посылки F1, F2 истинны, формула F1F2G может обратиться в ложь только, если |G| = F т.е. если |G| = T. Тогда логическое следствие выполнено. В принципе процедура опровержения форма­лизует метод редукции. Проблема поиска автоматического доказа­тельства при использовании процедуры опровержения значительно облегчается благодаря использованию так называемых «стандарт­ных» форм формул. Любую формулу логики предикатов можно привести к эквивалентной ей предваренной нормальной форме, когда все кванторы вынесены вперед, а в области действия кванто­ров формула находится в конъюнктивной нормальной форме. Если такая формула имеет только кванторы всеобщности, то она будет ложна, если найдется хотя бы одна интерпретация, которая обра­щает ее в ложь. Тогда эквивалентная ей исходная формула также будет ложна, а ее отрицание, соответственно, истинно. Если же среди кванторов имеются кванторы существования, то проблема услож­няется. Однако, кванторы существования можно снять (на основа­нии правила экзистенциальной конкретизации), в результате будет получена так называемая «скулемовская стандартная форма». Тогда поиск опровергающей интерпретации применяется к этой форме.