Тактики поиска вывода для локальных методов тема диссертации и автореферата по ВАК РФ 01.01.09, кандидат физико-математических наук Курьеров, Юрий Николаевич

• Курьеров, Юрий Николаевич
• кандидат физико-математических наук
• 1982

Оглавление диссертации кандидат физико-математических наук Курьеров, Юрий Николаевич

Введение.

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

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

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

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

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

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

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

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

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

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

Глава 3. Тактики основанные на строгом упорядочении литер.

§ I. Тактики с упорядочением типа ¿od. ,.

§ 2. Анализ возможности максимального упорядочения.

§ 3. Стратегия увеличения свободы выбора при распознавании пропозициональной выполнимости.

Введение диссертации (часть автореферата) на тему «Тактики поиска вывода для локальных методов»

К числу наиболее распространенных локальных методов установления доказуемости, в числе прочих, относятся метод резолюций [IX обратный метод [ 2 ] и ряд других. В диссертации уделяется основное внимание методу резолюций, хотя полученные результаты имеют место и для других локальных методов установления доказуемости. Зтот факт следует непосредственно из [17] , где показывается, что результаты, справедливые для одного локального метода, легко переносятся и на другие локальные методы.

Поиск вывода с использованием метода резолюций для произвольной формулы исчисления предикатовД^можно в общих чертах описать как процесс построения выводов в некотором специальном исчислении И(01)• Особенностью этого исчисления является то, что для каждой конкретной формулы строится свое исчисление. По каждой формуле ОС строится совокупность некоторых начальных объектов исходных конъюнктов, которые являются аксиомами для исчисления 1/1(01) . В этом исчислении введено единственное правило - правило резолюций, которое, исходя из множества исходных конъюнктов и полученных к моменту очередного применения правила резолюций, строит следующий конъюнкт. Этот процесс продолжается до тех пор пока не будет получен объект специального вида - пустой конъюнкт, который обозначается обычно через О .

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

Описанный процесс поиска вывода связан с перебором большого числа возможных применений правила резолюций. При этом, на каждом последующем шаге применения правила резолюций, число возможных применений будет возрастать. Поэтому, уже начиная с самых первых работ по локальным методам поиска вывода (в том числе и метода резолюций, как 'одного из представителей локальных методов установления доказуемоста) широко исследовался воцрос о способе ограничения перебора. Для этой цели используются так называемые тактики поиска вывода. Тактику поиска вывода в некотором исчислении можно описать как совокупность условий, ограничивающих применение правил вывода в этом исчислении. Ограничение возможности переборов возникает из-за того, что рассматриваются не все возможные выводы в исчислении И(ОС) , а только часть из них, удовлетворяющая данной тактике. При этом вполне возможно, что полученные выводы не будут наилучшими, т.е. не являются самыми короткими. Возможно, что для данной формулы 01 можно построить более короткий вывод. Однако применение тактики на каждом шаге поиска вывода сокращает число возможных применений правила резолюций. Таким образом, изучение тактик вывода представляет интерес не с точки зрения нахождения качественного вывода, а с точки зрения скорости нахождения какого-нибудь вывода.

Вопрос о полноте тактик вывода является одним из основных вопросов при рассмотрении тактик, т.к. полные тактики имеют то преимущество, что их можно применять при поиске вывода любых формул исчисления предикатов. Таких тактик за прошедшее время было разработано достаточно много. В числе различных работ, посвященных полни,! тактикам вывода, можно отметить Г2],Гз], Г83и целый ряд друг гих. Необходимо, правда, отметить, что положительные моменты, связанные с полнотой тактики, являются одновременно и их отрицательными сторонами. В самом деле, поскольку тактика вывода полна на исчислении предикатов, то она недостаточно подробно и в деталях учитывает особенности того или иного класса задач исчисления предикатов и, следовательно, не используются эти особенности для сокращения перебора. Поэтому, уже достаточно давно, помимо полных тактик, ведутся исследования по применению неполных тактик, которые бы были более ориентированы на тот или иной класс формул исчисления предикатов, точнее полны для этого класса формул. Следует отметить, что таких тактик и работ, их исследующих, значительно меньше, в том числе можно отметить следующие работы [7] и Г п1.

Все тактики, о которых говорилось выше, имеют одну характерную особенность (которая может рассматриваться с точки зрения ограничения перебора, как недостаток). В кавдом очередном применении правила резолюций обе посылки выбираются, вообще говоря, произвольно и независимо от результата предыдущего применения правила резолюций. Естественным желанием было бы исключить этот недостаток, т.е. разработать такую тактику, при которой кавдое последующее применение правила резолюций использовало бы результат непосредственно предшествующего ему правила резолюций. Нечто подобное имеет место в так называемой тактике исходных конъюнктов, описанной в [7] . Правда, эта тактика полна лишь на некотором, хоть и естестл венном, но специальном (Хорновском) классе формул исчисления предикатов.

Свое полное воплощение идея использования, на каждом шаге применения правила резолюций, в качестве одной из посылок результата непосредственно предшествующего применения правила резолюций, нашла в, так называемой, тактике линейного вывода, которая появилась приблизительно в то же время, что и тактика »описанная в работе [7"]. Эта тактика »ввиду своей структуры, представляется удобной для построения вычислительной процедуры. В последнее время она оказалась популярной. Исследованию этой тактики посвящен целый ряд работ (см, например [ 133 и [ 14]).

Необходимо отметить еде один класс тактик, исследование которого также занимает достаточно места в современных работах по поиску вывода. К таким тактикам относятся тактики с упорядочением членов, Их характерной особенностью является задание предварительно, до начала поиска вывода, некоего предиката, который контролирует и определяет порядок вхождений элементов в конъюнкт и, в зависимости от предварительного соглашения, тем самым определяет по какому элементу должно быть применение правила резолюций. Тем самым достигается ограничение свободы выбора посылок на том или ином шаге применения правила резолюций (см, [15] *[1в] ).

И, наконец, в последние годы появились работы, исследующие так называемые эвристические тактики, (см. [ 20] * [22] ). Характерным для этих тактик является существенная их неполнота не только на исчислении предикатов в целом, но и на его отдельных классах. С другой стороны, удачный выбор эвристики позволяет во многих, а то и в большинстве случаев получить вывод искомого специального объекта ( О ). При этом время, затрачиваемое на такой поиск, существенно меньше, чем цри использовании той или иной полной тактики.

Выше мы рассмотрели различные классы тактик поиска вывода. А что будет, если объединить две или более тактики? Возможен ж этот шаг вообще? Такие вопросы стаж появляться почти одновременно с появлением исследований, касающихся тактик поиска вывода. Необходимо отметить, что работ, так иж иначе затрагивающих эти вопросы, достаточно много. Можно в качестве примера сослаться на такие работы, как [2],[з],[83,[1з], [ 141 ц целый ряд других. Но здесь необходимо подчеркнуть, что все эти работы (иж, по крайней мере, большинство из них35-) рассматривают вопросы совместимости тактик иж их консервативности (т.е. возможности использования нескольких тактик одновременно дж поиска жшь конъюнкта □ иж любого выводимого конъюнкта, соответственно) жшь применительно к конкретным рассматриваемым тактикам. Это приводит к тому, что получаемые результаты носят частный характер, полученные утверждения для одних тактик не распространяются на сочетания других (в целом рассмотрение проблемы является очень громоздким).

Необходимо отметить и еще одно направление в исследовании выводов и тактик, которое в настоящее время недостаточно развито. Это анализ сложности поиска вывода и влияние тех иж иных тактик на сложность. Имеется ряд работ [43,[б], [б] и [17] , в которых поднимался вопрос о сложности вывода. Но в этих работах анажзиро-важсь жшь деревья вывода (причем минимальные) и никоим образом не затрагиважсь вопросы связанные с влиянием тех иж иных тактик на сложность вывода и, что цредставляется наиболее важным, на сложность поиска вывода.

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

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

В диссертации : для оценки сложности вывода по той или иной тактике использовался способ моделирования вывода на ЭВМ.

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

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

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

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

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

Диссертация состоит из введения, трех глав и двух приложений. Глава I состоит из 4 параграфов. В § I вводится основные определения, необходимые для формирования метода резолюций. Эти определения аналогичны соответствующим определениям из работы [II , Кроме того, формулируется понятие тактики взаимного поглощения (ВП-такти-ки), введенное в работе [21 . Применительно к ВБ-тактике обсуждается вопрос о сложности подстановочных термов в правиле резолюций, удовлетворяющем ВП-тактике, и приводится ряд примеров такого правила.

Список литературы диссертационного исследования кандидат физико-математических наук Курьеров, Юрий Николаевич, 1982 год

1. Робинсон Дж. Машинно-ориентированная логика, основанная на принципе резолюций, - В кн.: Кибернетический сборник, новая серия, ВШ1,7, М., Мир, 1970, с, 194-218.

2. Maslov S,Yu, Proof-Search Strategies for Methods of the Resolution Type, - In: Machine Intelligence, v. 6, Edihbur^, I97I, p. 77-90,

3. Замов H,K,, Шаронов В,И, Об одном классе стратегий, nppi- меняемых при установлении доказуемости методом резол1сций, - Зап. научн. семинаров. Ленингр. отд. Мат. ин-та АН СССР, 1969, т.16, с. 54-64.

4. Kuehner D. Some special purpose resolution systems.- I&chine Intelligence, v. 7, Edinburgh, 1972, p. II7-I28.

5. Курьеров Ю.Н. Условия полноты тактики линейного вывода. В кн.: Семантические вопросы искусственного интеллекта, Киев, 1977, с. 44-45.

6. Loveland D. А Linear Format for Resolution.- In: Lecture Notes in Mathematics, 1970, U 125, p. 147-162.

7. Andrews P. Resolution with Merging.- J. Assoc. Comput. Mach., 1968, V. 15, N 3, p. 367-381. поправки: J. Assoc. Comput. Mach., 1968, v. 15, N 4, p. 720.

8. Jouyner W. H. Jr. Resolution Strategies as Decision Procedures.- J. Assoc. Comput. Mach., 1976, v, 29, N 3, p« 398-417.

9. Маслов CIO, Информация в исчислении и рациона®!зация переборов. - Кибернетика, 1979, Ш 2, с. 20-26.

10. Курьеров Ю.Н. Об одном обобщении линейной тактики. - В кн.: Вопросы радиоэлектроники, серия ЭВТ, 1978, вып. 5, с, 85-91.

11. Курьеров Ю.Н. Тактика взаимного поглощения и ее нормальная форма. - Кибернетика. 1979, № 6, с. I38-I4I.

12. Курьеров Ю.Н. К вопросу о существовании строгой 1оск-ре- золщии. - В кн.: Семиотика и информатика. 1979, вып. 12, с. 23-29.

13. Курьеров Ю.Н. Линеаризация тшстики взаимного поглощения. - - В кн.: Искусственный интеллект и автоматизация исследований в математике: Тез. докл. и сообщений Всесоюзного симпозиума, Киев, 1978, с. 51-52. - 122 -

14. Курьеров Ю.Н., 1ласлов С Ю . Эксперимент с распознаванием пропозрпдиональной выполншлости на основе УС-стратегии. - 3 кн.: ' Математическая логика и математическая лингвистика. I98I, Калининский государственный университет, Калинин, с. I28-IS4.