Скачать 13.21 Кбайт
Обратный метод С.Ю. Маслова
Для сохранения теоремы о полноте исчисления необходимо потребовать хотя бы однократного применения правила Б в старой формулировке (применение правила Б по некоторому числу). Более строгое доказательство такой модификации дано в [13].
При внимательном рассмотрении схемы правила сечения, можно утверждать, что при применении "сверху вниз" правило сечения соответствует правилу резолюций: здесь также при "смешивании" двух дизъюнктов получается новый дизъюнкт за счет выбрасывания контрарной пары литер. Таким образом, получился своеобразный синтез обратного метода с методом резолюций.
Другим направлением модификации предложенного исчисления является минимизации числа благоприятных наборов, участвующих в выводе. Например, из приведенного анализа дерева вывода (смотри п.5 анализа после рис.1) напрашивается следующая модификация исчисления:
ЛЕММА 1
Если в некотором исходном благоприятном наборе встречается число с индексом такое, что полной совокупности индексов по данному числу нет, то все такие наборы без потери выводимости можно исключить из числа исходных благоприятных наборов.
Доказательство леммы очевидно: если правило Б в процессе построения вывода применяется к некоторому такому набору, то пустой благоприятный набор получить нельзя.
В нашем примере, без потери выводимости можно исключить следующие исходные благоприятные наборы 33 71 и 62 71
На основании леммы 1 возможно "подключить" к предложенной выше схеме исчисления следующую модификацию:
ЛЕММА 2
Если в составе исходных благоприятных наборов встречаются наборы, содержащие числа с индексом ноль, то все такие наборы, без потери выводимости, можно вычеркнуть, изменив индексацию других чисел этих наборов в остальных исходных благоприятных наборах.
Формулировка этой леммы основана на моделировании в исчислении известном для систем поиска вывода правила исключения однолитерных дизъюнктов: если в составе формулы встречается однолитерный дизъюнкт, то его можно без потери выводимости вычеркнуть из формулы, одновременно исключив из других дизъюнктов этой формулы литеры, контрарные литере этого однолитерного дизъюнкта [4]. Доказательство корректности этой леммы можно получить из допустимости правила исключения однолитерных дизъюнктов в секвенциальном исчислении.
Для минимизации числа "новых" благоприятных наборов, полученных по правилу Б можно предложить следующую лемму, которую можно назвать леммой о нормализации вывода:
ЛЕММА 3
При наличии среди уже имеющихся благоприятных наборов такого благоприятного набора, который является подмножеством некоторого вновь полученного благоприятного набора, использование этого нового благоприятного набора для получения вывода избыточно.
Данная лемма определяет целый класс эффективных стратегий построения выводов, так как сильно ограничивает число (вид) благоприятных наборов, участвующих в выводе: из процесса построения исключаются все наднаборы некоторого набора. На основании этого возможна не только нормализация вывода, но и дальнейшая модификация исходной "заготовки" исчисления следующим образом: "искусственное" введение в процесс построения выводов некоторых наборов — допущений, которые, например, одночленны (заметим, что этот подход близок идеологии систем натурального вывода, в которых использование допущений является существенной чертой при построении выводов). Тогда на основании лемм 1 и 2 возможно существенное сокращение исходных благоприятных наборов. Использование при построении выводов одночленных наборов — допущений связано с моделированием метода расщеплений. При моделировании правила расщеплений в секвенциальных исчислениях его можно трактовать как последовательное добавление к исходной формуле новых однолитерных дизъюнктов, полученных в результате "расщепления" некоторых дизъюнктов исходной формулы. Это является эквивалентным преобразованием формулы. За счет действия правила исключения однолитерных дизъюнктов количество дизъюнктов сокращается и вывод строится быстрее. В обратном методе возможно моделирование не только правила расщепления по некоторому дизъюнкту, но и моделирование нового правила расщепления по некоторому исходному благоприятному набору (см. правило Б). Технически это осуществлено в моей работе [14] (см. вставку (=ДОПОЛНЕНИЕ=) из этой работы ниже; ).
— данный текст дополнен фрагментом из работы: Катречко С.Л. Моделирование правила расщеплений в обратном методе С.Ю.Маслова //Логические методы в компьютерных науках. М., ИФ РАН, 1991). Здесь нам потребуется понятие набора с зависимостью, которое мы ввели ранее.
ДОПОЛНЕНИЕ ===== ** вставка из работы [14]
Моделирование правила расщепления в обратном методе
Использование при построении выводов одночленных наборов — допущений связано с моделированием метода расщеплений. При моделировании правила расщеплений в секвенциальных исчислениях его можно трактовать как последовательное добавление к исходной формуле новых однолитерных дизъюнктов, полученных в результате "расщепления" некоторых дизъюнктов исходной формулы.
При внимательном рассмотрении схемы правила сечения, можно утверждать, что при применении "сверху вниз" правило сечения соответствует правилу резолюций: здесь также при "смешивании" двух дизъюнктов получается новый дизъюнкт за счет выбрасывания контрарной пары литер. Таким образом, получился своеобразный синтез обратного метода с методом резолюций.
Другим направлением модификации предложенного исчисления является минимизации числа благоприятных наборов, участвующих в выводе. Например, из приведенного анализа дерева вывода (смотри п.5 анализа после рис.1) напрашивается следующая модификация исчисления:
ЛЕММА 1
Если в некотором исходном благоприятном наборе встречается число с индексом такое, что полной совокупности индексов по данному числу нет, то все такие наборы без потери выводимости можно исключить из числа исходных благоприятных наборов.
Доказательство леммы очевидно: если правило Б в процессе построения вывода применяется к некоторому такому набору, то пустой благоприятный набор получить нельзя.
В нашем примере, без потери выводимости можно исключить следующие исходные благоприятные наборы 33 71 и 62 71
На основании леммы 1 возможно "подключить" к предложенной выше схеме исчисления следующую модификацию:
ЛЕММА 2
Если в составе исходных благоприятных наборов встречаются наборы, содержащие числа с индексом ноль, то все такие наборы, без потери выводимости, можно вычеркнуть, изменив индексацию других чисел этих наборов в остальных исходных благоприятных наборах.
Формулировка этой леммы основана на моделировании в исчислении известном для систем поиска вывода правила исключения однолитерных дизъюнктов: если в составе формулы встречается однолитерный дизъюнкт, то его можно без потери выводимости вычеркнуть из формулы, одновременно исключив из других дизъюнктов этой формулы литеры, контрарные литере этого однолитерного дизъюнкта [4]. Доказательство корректности этой леммы можно получить из допустимости правила исключения однолитерных дизъюнктов в секвенциальном исчислении.
Для минимизации числа "новых" благоприятных наборов, полученных по правилу Б можно предложить следующую лемму, которую можно назвать леммой о нормализации вывода:
ЛЕММА 3
При наличии среди уже имеющихся благоприятных наборов такого благоприятного набора, который является подмножеством некоторого вновь полученного благоприятного набора, использование этого нового благоприятного набора для получения вывода избыточно.
Данная лемма определяет целый класс эффективных стратегий построения выводов, так как сильно ограничивает число (вид) благоприятных наборов, участвующих в выводе: из процесса построения исключаются все наднаборы некоторого набора. На основании этого возможна не только нормализация вывода, но и дальнейшая модификация исходной "заготовки" исчисления следующим образом: "искусственное" введение в процесс построения выводов некоторых наборов — допущений, которые, например, одночленны (заметим, что этот подход близок идеологии систем натурального вывода, в которых использование допущений является существенной чертой при построении выводов). Тогда на основании лемм 1 и 2 возможно существенное сокращение исходных благоприятных наборов. Использование при построении выводов одночленных наборов — допущений связано с моделированием метода расщеплений. При моделировании правила расщеплений в секвенциальных исчислениях его можно трактовать как последовательное добавление к исходной формуле новых однолитерных дизъюнктов, полученных в результате "расщепления" некоторых дизъюнктов исходной формулы. Это является эквивалентным преобразованием формулы. За счет действия правила исключения однолитерных дизъюнктов количество дизъюнктов сокращается и вывод строится быстрее. В обратном методе возможно моделирование не только правила расщепления по некоторому дизъюнкту, но и моделирование нового правила расщепления по некоторому исходному благоприятному набору (см. правило Б). Технически это осуществлено в моей работе [14] (см. вставку (=ДОПОЛНЕНИЕ=) из этой работы ниже; ).
— данный текст дополнен фрагментом из работы: Катречко С.Л. Моделирование правила расщеплений в обратном методе С.Ю.Маслова //Логические методы в компьютерных науках. М., ИФ РАН, 1991). Здесь нам потребуется понятие набора с зависимостью, которое мы ввели ранее.
ДОПОЛНЕНИЕ ===== ** вставка из работы [14]
Моделирование правила расщепления в обратном методе
Использование при построении выводов одночленных наборов — допущений связано с моделированием метода расщеплений. При моделировании правила расщеплений в секвенциальных исчислениях его можно трактовать как последовательное добавление к исходной формуле новых однолитерных дизъюнктов, полученных в результате "расщепления" некоторых дизъюнктов исходной формулы.
|
|