Скачать 13.21 Кбайт
Обратный метод С.Ю. Маслова
Такой "механизм работы" секвенциальных исчислений основан на свойстве подформульности, которое после доказательство Г. Генценом теоремы об устранимости сечения [9] получило универсальный характер.
Другой важной особенностью секвенциальных исчислений является обратимость правил вывода. Так как все правила построения дерева поиска вывода применимы не только снизу вверх, но и сверху вниз, то возможно "автоматическое" превращение дерева поиска вывода в дерево вывода.
Именно эти особенности секвенциальных исчислений сделали их удобным аппаратом для выполнения "механического" построения выводов: подформульность исчислений гарантирует окончание процесса "расщепления" любой сложной формулы до элементарных подформул, а обратимость правил вывода — превращение "заготовки" вывода при определенных условиях в вывод. С другой стороны, эта машинообразность процедуры поиска приводит к неэффективности поиска вывода и резкому увеличению сложности вывода при увеличении сложности исходных формул. Возникает проблема так называемого экспоненциального взрыва. Связано это с тем, что в секвенциальных исчислениях строится полное дерево поиска вывода "слепым перебором". При этом приходится "проделывать" много лишней работы, которая и ведет, в конечном итоге, к резкому увеличению сложности вывода. "Открытие" этого факта в логике в 70-е годы привело, с одной стороны, к бурному развитию АДТ, в котором пытаются преодолеть неэффективность аналитических исчислений, а с другой стороны, к появлению новой дисциплины — теории сложности, в рамках которой было осознано, что проблема экспоненциального взрыва имеет принципиальный характер и для решения этой проблемы (в общем виде она получила название P = NP — проблемы) необходимы принципиально новые подходы [10].
Одним из возможных подходов к повышению эффективности поиска вывода является идея глобальной обработки информации, которая была предложена в 60-е годы одновременно советским логиком Н.А. Шаниным и шведским логиком С. Кангером. Суть идеи заключается в попытке более полного использования информации о структуре формулы и уже полученного дерева поиска вывода и за счет этого сделать поиск вывода более "разумным".
С одной стороны, при отсутствии необходимой информации предварительно строится некоторая "заготовка" вывода, которую при получении недостающей информации можно либо превратить в вывод, либо отрицательно ответить на вопрос о выводимости данной формулы. Для исчисления предикатов эта идея находит выражение в использовании при поиске вывода новых объектов, метапеременных, которые позволяют без необходимости не конкретизировать вывод при отсутствии достаточной информации [см. ст. С. Кангера в 9].
С другой стороны, используя полученную информация о структуре формулы и уже полученного дерева вывода, можно попробовать исключить из дерева поиска ту информацию, которая является избыточной для построения вывода или дублирует информацию, содержащуюся в других частях дерева поиска. Т.е. при построении дерева поиска вывода использовать "глобальную" информацию всего дерева. Это направление идеи "глобальной обработки информации" получило развитие в работах группы ленинградских логиков под руководством Н.А. Шанина [11].
Обратный метод и представляет собой дальнейшее развитие особенностей секвенциальных исчислений с учетом идеи "глобальной обработки информации".
Во-первых, получила дальнейшее развитие идея анализа информации, заключенной в исходной формуле. Исчисления обратного метода строятся для каждой конкретной формулы, которую необходимо доказать. По виду исходной формулы, в понятии исходного благоприятного набора, определяется вид только тех аксиом, которые могут быть "полезны" для построения вывода данной формулы. Все остальное бесконечное множество аксиом не используется.
Во-вторых, в обратном методе существенным образом используется обратимость правил секвенциальных исчислений: так как правила поиска вывода, применяемые "снизу вверх" при поиске, могут быть использованы "сверху вниз" при построении дерева вывода, то возможно создание "универсального" механизма построения дерева вывода "сверху вниз" - правило Б обратного метода. Тем самым, обратный метод еще раз "перевернул" направление построения дерева вывода по сравнению с секвенциальными исчислениями. Именно с этим обращением направления поиска и связано название обратного метода.
Возможно предложить целый класс исчислений обратного метода, которые дополняют общие идеи ОМ различными тактиками поиска. Поэтому сначала сформулируем некоторую общую схему обратного метода для исчисления высказываний, и затем покажем возможности его "обогащения" за счет моделирования различных эвристик.
Технически такие исчисления в данной статье построены для формул исчисления высказываний в дизъюнктивной нормальной форме.
ОБЩАЯ СХЕМА ОБРАТНОГО МЕТОДА
Пусть нам дана некоторая формула Ф в дизъюнктивной нормальной форме, где графически равные дизъюнкты и конъюнкты сокращены до одного, и секвенциальное исчисление, в котором необходимо установить выводимость данной формулы.
Другой важной особенностью секвенциальных исчислений является обратимость правил вывода. Так как все правила построения дерева поиска вывода применимы не только снизу вверх, но и сверху вниз, то возможно "автоматическое" превращение дерева поиска вывода в дерево вывода.
Именно эти особенности секвенциальных исчислений сделали их удобным аппаратом для выполнения "механического" построения выводов: подформульность исчислений гарантирует окончание процесса "расщепления" любой сложной формулы до элементарных подформул, а обратимость правил вывода — превращение "заготовки" вывода при определенных условиях в вывод. С другой стороны, эта машинообразность процедуры поиска приводит к неэффективности поиска вывода и резкому увеличению сложности вывода при увеличении сложности исходных формул. Возникает проблема так называемого экспоненциального взрыва. Связано это с тем, что в секвенциальных исчислениях строится полное дерево поиска вывода "слепым перебором". При этом приходится "проделывать" много лишней работы, которая и ведет, в конечном итоге, к резкому увеличению сложности вывода. "Открытие" этого факта в логике в 70-е годы привело, с одной стороны, к бурному развитию АДТ, в котором пытаются преодолеть неэффективность аналитических исчислений, а с другой стороны, к появлению новой дисциплины — теории сложности, в рамках которой было осознано, что проблема экспоненциального взрыва имеет принципиальный характер и для решения этой проблемы (в общем виде она получила название P = NP — проблемы) необходимы принципиально новые подходы [10].
Одним из возможных подходов к повышению эффективности поиска вывода является идея глобальной обработки информации, которая была предложена в 60-е годы одновременно советским логиком Н.А. Шаниным и шведским логиком С. Кангером. Суть идеи заключается в попытке более полного использования информации о структуре формулы и уже полученного дерева поиска вывода и за счет этого сделать поиск вывода более "разумным".
С одной стороны, при отсутствии необходимой информации предварительно строится некоторая "заготовка" вывода, которую при получении недостающей информации можно либо превратить в вывод, либо отрицательно ответить на вопрос о выводимости данной формулы. Для исчисления предикатов эта идея находит выражение в использовании при поиске вывода новых объектов, метапеременных, которые позволяют без необходимости не конкретизировать вывод при отсутствии достаточной информации [см. ст. С. Кангера в 9].
С другой стороны, используя полученную информация о структуре формулы и уже полученного дерева вывода, можно попробовать исключить из дерева поиска ту информацию, которая является избыточной для построения вывода или дублирует информацию, содержащуюся в других частях дерева поиска. Т.е. при построении дерева поиска вывода использовать "глобальную" информацию всего дерева. Это направление идеи "глобальной обработки информации" получило развитие в работах группы ленинградских логиков под руководством Н.А. Шанина [11].
Обратный метод и представляет собой дальнейшее развитие особенностей секвенциальных исчислений с учетом идеи "глобальной обработки информации".
Во-первых, получила дальнейшее развитие идея анализа информации, заключенной в исходной формуле. Исчисления обратного метода строятся для каждой конкретной формулы, которую необходимо доказать. По виду исходной формулы, в понятии исходного благоприятного набора, определяется вид только тех аксиом, которые могут быть "полезны" для построения вывода данной формулы. Все остальное бесконечное множество аксиом не используется.
Во-вторых, в обратном методе существенным образом используется обратимость правил секвенциальных исчислений: так как правила поиска вывода, применяемые "снизу вверх" при поиске, могут быть использованы "сверху вниз" при построении дерева вывода, то возможно создание "универсального" механизма построения дерева вывода "сверху вниз" - правило Б обратного метода. Тем самым, обратный метод еще раз "перевернул" направление построения дерева вывода по сравнению с секвенциальными исчислениями. Именно с этим обращением направления поиска и связано название обратного метода.
Возможно предложить целый класс исчислений обратного метода, которые дополняют общие идеи ОМ различными тактиками поиска. Поэтому сначала сформулируем некоторую общую схему обратного метода для исчисления высказываний, и затем покажем возможности его "обогащения" за счет моделирования различных эвристик.
Технически такие исчисления в данной статье построены для формул исчисления высказываний в дизъюнктивной нормальной форме.
ОБЩАЯ СХЕМА ОБРАТНОГО МЕТОДА
Пусть нам дана некоторая формула Ф в дизъюнктивной нормальной форме, где графически равные дизъюнкты и конъюнкты сокращены до одного, и секвенциальное исчисление, в котором необходимо установить выводимость данной формулы.
|
|