Тактики поиска вывода для локальных методов

• Автор: Курьеров, Юрий Николаевич
• Шифр специальности: 01.01.09
• Научная степень: Кандидатская
• Год защиты: 1982
• Место защиты: Ленинград
• Количество страниц: 123 c. : ил

Глава I. Тактика взаимного поглощения и ее нормальная форма

§ I. Определение тактики взаимного поглощения

§ 2. Полнота тактики взаимного поглощения. Нормальная

форма вывода

§ 3. Совместимость тактики взаимного поглощения и тактики избегания противоречивых конъюнктов

§ 4. Сравнение сложности деревьев поиска вывода по

ВП-тактике и ВП-тактике без противоречий

Глава 2. Возможности линеаризации тактик

§ I. Условия полноты ИК-тактики

§ 2. Обобщение тактики линейного вывода

§ 3. Усиление тактики линейного вывода

Глава 3. Тактики основанные на строгом упорядочении литер
§ I. Тактики с упорядочением типа
§ 2. Анализ возможности максимального упорядочения
§ 3. Стратегия увеличения свободы выбора при распознавании пропозициональной выполнимости
Приложение 1
Приложение 1
Литература

ПОСВЯЩАЕТСЯ светлой памяти моего учителя Сергея Юрьевича Маслова
К числу наиболее распространенных локальных методов установления доказуемости, в числе прочих, относятся метод резолюций С 1*1» обратный метод [ 2 ] и ряд других. В диссертации уделяется основное внимание методу резолюций, хотя полученные результаты имеют место и для других локальных методов установления доказуемости. Зтот факт следует непосредственно из [І7І , где показывается, что результаты, справедливые для одного локального метода, легко переносятся и на другие локальные методы.
Поиск вывода с использованием метода резолюций для произвольной формулы исчисления предикатов ^мокно в общих чертах описать как процесс построения выводов в некотором специальном исчислении ИМ Особенностью этого исчисления является то, что для каждой конкретной формулы строится саое исчисление. По каждой формуле 0{, строится совокупность некоторых начальных объектов исходных конъюнктов, которые являются аксиомами для исчисления И(О^)
В этом исчислении введено единственное правило - правило резолюций, которое, исходя из множества исходных конъюнктов и полученных к моменту очередного применения правила резолюций, строит следующий конъюнкт. Зтот процесс продолжается до тех пор пока не будет получен объект специального вида - пустой конъюнкт, который обозначается обычно через О
Получение в результате применения правила резолюций конъюнкта О означает то, что формула 0^ доказуема. Если в результате
применения правила резолюций к конечному множеству конъюнктов получаются лишь конъюнкты из того же множества конъюнктов, то это означает, что формула ОС не доказуема. Однако, хорошо известен . результат о неразрешимости исчисления предикатов, поэтому в общем случае для недоказуемых формул процесс поиска вывода может продолжаться как угодно долго.
Описанный процесс поиска вывода связан с перебором большого числа возможных применений правила резолюций. При этом, на каждом последующем шаге применения правила резолюции, число возможных применений будет возрастать. Поэтому, уже начиная с самых первых работ по локальным методам поиска вывода (в том числе и метода резолюций, как 'одного из представителей локальных методов установления доказуемости) широко исследовался вопрос о способе ограничения перебора. Для этой цели используются так называемые тактики поиска вывода. Тактику поиска вывода в некотором исчислении можно описать как совокупность условий, ограничивающих применение правил вывода в этом исчислении. Ограничение возможности переборов возникает из-за того, что рассматриваются не все возможные выводы в исчислении И(ос') , а только часть из них, удовлетворяющая данной тактике. При этом вполне возможно, что полученные выводы не будут наилучшими, т.е. не являются самыми короткими. Возможно, что для данной формулы 01 можно построить более короткий вывод. Однако применение тактики на каждом шаге поиска вывода сокращает число возможных применений правила резолюций. Таким образом, изучение тактик вывода представляет интерес не с точки зрения нахождения качественного вывода, а с точки зрения скорости нахождения какого-нибудь вывода.
Вопрос о полноте тактик вывода является одним из основных

конъюнкт, вводящий эту литеру, может находиться в линейной ветви Ч только строго выше того применения , где эта литера выводится. Но ввиду регулярности резольвента применения этого исходного конъюнкта с резольвентой предыдущего применения одного из шагов 3 + 7 алгорифма /^непротиворечива. Следовательно, резольвента останется непротиворечивой и в случае, когда этот конъюнкт, как самый верхний, вводящий интересующую литеру, принадлежит . Дальнейшие применения алгорифма ^рассмотрены выше и составляют случай (I).
Случай (III) в алгорифме 01, вследствие п.п. 2 и 3, исключается. Отметим также, что переход из одного связного блока в другой возможно единственным способом, а именно, по литере того ИК-приме-нения, которое было первым на соответствующем применении алгорифма (^(рассматриваются шаги 3 + 7 алгорифма 01) * Этим доказана непротиворечивость применения шагов 3 + 7 алгорифма«^для случая (б).
Это является базой индукции, т.к. на шагах 8 + II непротиворечивость очевидна.
Далее проведем индукцию по количеству применений алгорифма 00 к линейной ветви о£ . Индукционный шаг аналогичен рассмотрению случая (б). Закончив индукцию по количеству применений 01 К оС , проведем аналогичную индукцию по количеству применений 01 к Чі вида
(I), где уже и Ч и лсевдорегулярны для % . (Индукция легко

проходат по числу регулярных блоков).
Таким образом получается следующий обобщающий теорему 1.4. результат.
Теорема 1.5. Если при перестроении регулярного вывода Ч конъюнкта П используется алгорифм 01 и в процессе его применения возникают псевдорегулярные для Ч линейные ветви Ч± Чи , то применения алгорифма 01 к линейным ветвям % ,...» Чп не приводят к появлению противоречивых резольвент.