Занятие 6. Логическое следствие в исчислении предикатов

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

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

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

В 1964-1965 гг. независимо друг от друга появились обратный метод установления выводимости Маслова и принцип резолюции Робинсона. Процедура поиска доказательства методом резолюции оказалась много эффективней, чем все предыдущие процедуры.

В те же годы Шаниным и его коллегами было разработано несколько версий алгоритма машинного поиска естественного логического вывода в исчислении

высказываний (АЛПЕВ). Разработка версий системы АЛПЕВ и машинных алгоритмов вывода на основе обратного метода и принципа резолюции показала принципиальную возможность машинного доказательства теорем.

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

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

Дата добавления: 2015-06-27