Скачать 13.21 Кбайт
Обратный метод С.Ю. Маслова
Но любое применение правила Б соответствует "получению" в секвенциальном выводе некоторого дизъюнкта исходной формулы Ф. При этом возможно получение не всех дизъюнктов исходной формулы. Например, для приведенной формулы Ф правило Б не будет применяться к литерам дизъюнкта под номером 7 (к числам с номером 7), а это значит, что будет получен вывод более сильной формулы Ф* без последнего дизъюнкта формулы Ф. Значит при получении пустого набора будет получено доказательство формулы Ф*, которая не слабее формулы Ф. Теорема доказана.
Таким образом, полученное исчисление, с одной стороны, эквивалентно в смысле выводимости исходному секвенциальному исчислению и позволяет "кодировать" выводы целого класса формул определенной структуры. Благодаря анализу информации о структуре формулы и учету особенностей построения секвенциальных выводов удалось частично избавиться от "слепого перебора", характерного для секвенциальных исчислений. Построение выводов стало более осмысленным.
С другой стороны, процесс построения вывода утратил свойство "нормальности" секвенциальных исчислений и приобрел более творческий характер. В процессе построения выводов возможно порождение кусков дерева, которые не приводят к успеху. При применении правила Б возможно порождение множества благоприятных наборов, которые избыточны для построения выводов. Возникает проблема повышения эффективности предложенной общей схемы обратного метода.
Возможны следующие подходы решения проблемы повышения эффективности предложенной "заготовки" исчисления:
1. Модификация предложенной схемы за счет "подключения" различного рода эвристик и допустимых правил вывода, которые повышают мощность первоначальной "заготовки" исчисления. В этом случае "сфера действия" правила Б расширяется.
2. Модификация предложенного исчисления за счет ограничения числа благоприятных наборов, участвующих в выводе. В данном случае "сфера действия" правила Б ограничивается.
Отметим, что данные подходы противоречат друг другу, но лишь отчасти.
МОДИФИКАЦИИ ОБЩЕЙ СХЕМЫ ОБРАТНОГО МЕТОДА.
МОДЕЛИРОВАНИЕ ПРАВИЛА РЕЗОЛЮЦИЙ
Как было отмечено выше, исчисления благоприятных наборов являются удобным базисом для моделирования различных правил вывода и эвристик, соответствующим разным методам автоматического теорем. Как известно из литературы [12], важным средством повышения мощности (эффективности) систем поиска вывода является моделирование в них правила сечения. Для сформулированного выше секвенциального исчисления правило сечения является допустимым. Сравним правило сечения с правилом Б исчисления благоприятных наборов. Для этого запишем их следующим образом:
правило вывода Б исчисления правило сечения
® A, X ® B, Y ® A, C ® B, ~C
® A, B, X & Y ® A, B, C & ~C
® A, B (F) ® A, B
Здесь X & Y можно исключить правилу Здесь C & ~C можно исключить по правилу
вывода исчисления, при условии, что сечения, так как C & ~C — противоречие и его
X & Y образуют формулы Ф. удаление не нарушает выводимости ® A, B
Как видно из приведенного рисунка "механизм работы" этих двух правил аналогичен, т.е. налицо структурное сходство. Правило Б можно понимать как аналог правила сечения, который при своем применении сверху вниз, также как и правило сечения позволяет исключать некоторые литеры, которые встречались в верхней части правил. Если правило сечения исключает те литеры, которые образуют контрарные пары, то правило Б — литеры, которые образуют некоторый дизъюнкт исходной формулы Ф. И в том, и в другом случае преобразования сохраняют эквивалентность формул.
Для моделирования правила сечения можно предложить следующую модификацию правила Б:
ПРАВИЛО Б*: При образовании благоприятных наборов разрешено выбрасывать не только те числа с индексами, которые составляют полную совокупность по некоторому числу, но и те числа с индексами, которые образуют один из исходных благоприятных наборов.
"Сфера действия" двухпосылочного правила Б расширяется: теперь при "склеивании" благоприятных наборов разрешается выбрасывать контрарные пары литер. Такая модификация правила Б и соответствует моделированию правила сечения относительно формулы Ф, поскольку применение правила Б по некоторому исходному благоприятному набору и соответствует выбрасыванию из состава формулы контрарных пар литер. При этом, возможности исходного исчисления расширяются. Теперь эти исчисления можно использовать для установления ложности формул: если при построении вывода применять правило Б только по исходным благоприятным наборам, то получение пустого благоприятного набора позволяет сделать вывод о том, что в составе исходной формулы Ф содержатся только противоречивые дизъюнкты и, следовательно, формула Ф тождественно — ложна.
Таким образом, полученное исчисление, с одной стороны, эквивалентно в смысле выводимости исходному секвенциальному исчислению и позволяет "кодировать" выводы целого класса формул определенной структуры. Благодаря анализу информации о структуре формулы и учету особенностей построения секвенциальных выводов удалось частично избавиться от "слепого перебора", характерного для секвенциальных исчислений. Построение выводов стало более осмысленным.
С другой стороны, процесс построения вывода утратил свойство "нормальности" секвенциальных исчислений и приобрел более творческий характер. В процессе построения выводов возможно порождение кусков дерева, которые не приводят к успеху. При применении правила Б возможно порождение множества благоприятных наборов, которые избыточны для построения выводов. Возникает проблема повышения эффективности предложенной общей схемы обратного метода.
Возможны следующие подходы решения проблемы повышения эффективности предложенной "заготовки" исчисления:
1. Модификация предложенной схемы за счет "подключения" различного рода эвристик и допустимых правил вывода, которые повышают мощность первоначальной "заготовки" исчисления. В этом случае "сфера действия" правила Б расширяется.
2. Модификация предложенного исчисления за счет ограничения числа благоприятных наборов, участвующих в выводе. В данном случае "сфера действия" правила Б ограничивается.
Отметим, что данные подходы противоречат друг другу, но лишь отчасти.
МОДИФИКАЦИИ ОБЩЕЙ СХЕМЫ ОБРАТНОГО МЕТОДА.
МОДЕЛИРОВАНИЕ ПРАВИЛА РЕЗОЛЮЦИЙ
Как было отмечено выше, исчисления благоприятных наборов являются удобным базисом для моделирования различных правил вывода и эвристик, соответствующим разным методам автоматического теорем. Как известно из литературы [12], важным средством повышения мощности (эффективности) систем поиска вывода является моделирование в них правила сечения. Для сформулированного выше секвенциального исчисления правило сечения является допустимым. Сравним правило сечения с правилом Б исчисления благоприятных наборов. Для этого запишем их следующим образом:
правило вывода Б исчисления правило сечения
® A, X ® B, Y ® A, C ® B, ~C
® A, B, X & Y ® A, B, C & ~C
® A, B (F) ® A, B
Здесь X & Y можно исключить правилу Здесь C & ~C можно исключить по правилу
вывода исчисления, при условии, что сечения, так как C & ~C — противоречие и его
X & Y образуют формулы Ф. удаление не нарушает выводимости ® A, B
Как видно из приведенного рисунка "механизм работы" этих двух правил аналогичен, т.е. налицо структурное сходство. Правило Б можно понимать как аналог правила сечения, который при своем применении сверху вниз, также как и правило сечения позволяет исключать некоторые литеры, которые встречались в верхней части правил. Если правило сечения исключает те литеры, которые образуют контрарные пары, то правило Б — литеры, которые образуют некоторый дизъюнкт исходной формулы Ф. И в том, и в другом случае преобразования сохраняют эквивалентность формул.
Для моделирования правила сечения можно предложить следующую модификацию правила Б:
ПРАВИЛО Б*: При образовании благоприятных наборов разрешено выбрасывать не только те числа с индексами, которые составляют полную совокупность по некоторому числу, но и те числа с индексами, которые образуют один из исходных благоприятных наборов.
"Сфера действия" двухпосылочного правила Б расширяется: теперь при "склеивании" благоприятных наборов разрешается выбрасывать контрарные пары литер. Такая модификация правила Б и соответствует моделированию правила сечения относительно формулы Ф, поскольку применение правила Б по некоторому исходному благоприятному набору и соответствует выбрасыванию из состава формулы контрарных пар литер. При этом, возможности исходного исчисления расширяются. Теперь эти исчисления можно использовать для установления ложности формул: если при построении вывода применять правило Б только по исходным благоприятным наборам, то получение пустого благоприятного набора позволяет сделать вывод о том, что в составе исходной формулы Ф содержатся только противоречивые дизъюнкты и, следовательно, формула Ф тождественно — ложна.
|
|