автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Программная система КВАНТ/1 для автоматического доказательства теорем

1 Введение

1.1 Актуальность задачи АДТ и предмет диссертации.

1.2 Теоретическая база создания программной системы КВАНТ/1 И

1.2.1 Язык Ь по-формул.И

1.2.2 Исчисление 3 по-формул.

1.3 Цели и структура работы.

1.4 Научная новизна, практическая значимость и апробация полученных результатов.

2 Алгоритмическое обеспечение программной системы КВАНТ/

2.1 Структуры данных для представления по-формул.

2.2 Алгоритмы автоматического доказательства теорем в исчислении /.

2.2.1 Организация перебора вопросов и подстановок

2.2.2 Поиск ответной подстановки.

2.2.3 Преобразование базовой подформулы в ходе шага вывода

3 Программная система КВАНТ/1: реализация и использование

3.1 Назначение и область применения программной системы

3.2 Архитектура системы

3.3 Методика использования

3.4 Огранизация взаимодействия и управления.

3.4.1 Язык управления.

3.4.2 Интерфейс прикладного уровня

3.5 Реализация.

3.5.1 Представление по-формул в памяти ЭВМ.

3.5.2 Реализация базовых алгоритмов АДТ.

3.5.3 Реализация вспомогательных алгоритмов.

4 Применения програмного комплекса

4.1 Задача Л.Шуберта о "паровом катке"

4.2 Задача наведения телескопа на центр планеты в неполной фазе

1.1 Актуальность задачи АДТ и предмет диссертации

Автоматическое доказательство теорем (АДТ) — перспективное направление в области искусственного интеллекта (ИИ), которое основывается на методах математической логики (теории доказательств) и реализуется в компьютерных программах автоматического поиска логического вывода (ЛВ).

Одной из пионерных разработок в истории применения ЭВМ для автоматического доказательства теорем (АДТ) является программа "Логик — Теоретик" (А. Newell, J. С. Shaw, Н. A. Simon [1, 2]), созданная авторами для доказательства теорем в исчислении высказываний (1956 г.). Программа доказала часть теорем из "Principia Mathematica" [3].

В I960 г. Дж. Гелернтером была создана программа автоматического доказательства теорем из школьной математики, которая "доказывала теоремы лучше, чем ее создатель" [4, 5]. Как и "Логик — Теоретик", она доказывала теоремы, используя строго формализованные аксиомы, а механизм вывода моделировал содержательные математические рассуждения примерно в том виде, в каком они осуществляются человеком [6]. Дж. Гелерн-тер указал на то, что в процессе доказательства, как правило, имелось достаточно много вариантов (путей), по которым можно было осуществлять поиск вывода, причем большинство из них приводили в тупик. Чтобы помочь программе сфокусировать поиск на перспективных направлениях, он добавил возможность представлять некоторый частный случай общей теоремы в виде численной диаграммы, на основе которой делались те или иные предпочтения дальнейшего вывода. Кроме того, была реализована дополнительная возможность, а именно, перед тем, как программа пыталась доказать теорему, она проверяла выводимость некоторого частного ее случая и только при удачном исходе имело смысл продолжать основной поиск вывода. Реализация программы осуществлена на языке ЛИСП: система производила манипуляции со списками атомов, представляющими геометрические фигуры.

В этом же 1960 г. Ван Хао создал ряд программ АДТ [7], первая из которых "переборола" программу "Логик — Теоретик" по количеству доказанных теорем исчисления высказываний из "Principia Mathematica". Программа осуществляла доказательство в секвенциальном исчислении с оди-надцатью правилами вывода и одной схемой аксиом. Наряду с этим, она использовалась для поиска новых теорем из синтезируемых формул. Две другие программы доказывали теоремы в исчислении предикатов и в некоторых его подклассах с использованием различных стратегий.

Еще одним примером использования подобного подхода к доказательству в формальной логике стал так называемый "обратный метод" поиска вывода [8], предложенный С. Ю. Масловым в 1965 г. Поиск вывода строился от целевой формулы к аксиомам или постулатам, истинность которых априорно известна. Вывод осуществлялся в первопорядковом исчислении предикатов с использованием процедур унификации. На основе этого метода разработаны машинный алгоритм вывода [9] и несколько версий алгоритма машинного поиска так называемого естественного вывода в исчислении высказываний (АЛПЕВ) [10]. Разработка версий систем АЛПЕВ—ЛОМИ и алгоритма вывода на основе обратного метода носила поисковый характер и показала принципиальную возможность машинных доказательств теорем.

Началом этапа бурного развития методов и программных систем АДТ послужило открытие подхода, основанного на приведении рассуждений к противоречию с помощью единственного и простого правила вывода — правила резолюции, предложенного в том же 1965 г. Дж. Робинсоном [11]. Вывод строился в направлении получения формулы-следствия, явно содержащей противоречие, а именно, получения пустого дизъюнкта, эквивалентного лжи. Основным достоинством метода явилась его механическая (машинная) направленность, в которой процедура вывода была (первоначально) достаточно проста и легко реализуема. Принцип резолюции успешно использовался для прикладных систем ИИ, основанных на доказательстве теорем (Слейгл, Грин, Ковальский) и, в частности, для верификации программ (Кинг, Уолдингер). Метод резолюции оказал значительное влияние на развитие области АДТ в целом [6]. В литературе известны статьи, исследующие синтез обратного метода Маслова и метода резолюции [12], имеющих примерно одинаковую силу.

Важной вехой в развитии приложений АДТ послужили работы Boca [13], в которых описан опыт применения программы АДТ AURA для решения открытых проблем дискретной математики и некоторых технических задач. Основным результатом этой работы явилось обоснование необходимости использования таких программ при решении задач математики и математической логики. Кроме того, большое внимание уделено технологии их использования в научной работе.

В Иркутске в 1970-80 гг. были созданы две системы автоматического получения на ЭВМ нетривиальных математических теорем: одна — как система автоматического синтеза теорем в терминах функций типа Ляпунова, морфизмов и их аналогов (пакет программ "ВФЛ-1") [14, 15, 16], а другая — как система интерактивного доказательства теорем на основе так называемых инвариантных преобразований (АВТОДОТ) [17]. С методологической точки зрения, обе системы базировались на так называемом алгоритмизационном подходе, основанном на выявлении и алгоритмизации основных приемов формулирования и доказательства теорем [18]. Позднее в работе [19] было достигнуто усиление системы автоматического синтеза теорем "ВФЛ-1" применением методов решения первопорядковых логических уравнений [20] и некоторых дедуктивных средств так называемого по-исчисления [21]. Кроме того, некоторый конструктивный фрагмент по-исчисления был использован в [22] для планирования вычислений.

В компьютерной реализации АДТ, ориентированной на создание интеллектуальных вопросно-ответных систем, систем верификации программ, тестирования схем, планирования вычислений и т.п. нашли широкое применение логические и функциональные языки программирования. Среди них наиболее популярны LISP1 и ПРОЛОГ2.

Язык ЛИСП — это первый функциональный язык, теоретической основой которого является À-исчисление Чёрча [23]. Язык разработан Дж. Мак-карти в начале 60-х годов [24] и быстро завоевал популярность среди программистов, проектирующих системы ИИ. Основным его свойством, привлекающим разработчиков, является эффективное представление и обработка символьной информации. Вероятно, ЛИСП был первым таким языком, и, отчасти, из-за этого получил большую популярность в ИИ. Программа языка ЛИСП представляет собой такую же структуру данных, как и данные, ею обрабатываемые, что дает возможность изменять программу

1От англ. LISt Processing — обработка списков.

2От англ. PROLOG — PROgramming in terms of LOGic. в процессе ее исполнения.

Другим, не менее важным языком программирования, разработанным А. Кольмерауэром в 1971 г. [25] и оказавшим значительное влияние на ИИ в целом, является язык ПРОЛОГ. Как и ЛИСП, ПРОЛОГ является инструментом для обработки символьной информации, но, в отличие от ЛИСПа, правила преобразования здесь представляются не в виде функций, а в виде логических правил, представляемых хорновскими формулами. Чуть позже Р. Ковальский обнаружил этот конструктивный смысл хорновских формул [26], что дало теоретическое обоснование процедурной семантике, лежащей в основе этого языка.

Реализации обоих языков можно разбить на две группы. В первую группу попадают системы, где программа в исходном языке интерпретируется другой программой. Ко второй группе относятся системы, которые первоначально транслируют исходную программу в код некоторой абстрактной машины, а затем производится интерпретация этого кода. Среди реализаций этого механизма в среде ЛИСП наиболее известны МФП3-система и G-система. Для ПРОЛОГА разработана подобная машина, называемая машиной Уоррена [27, 28].

ПРОЛОГ в своей основе реализует идеи и принципы метода резолюции, а именно включает:

1) SLD-резолюцию [29] как основной механизм вывода; при этом используется стратегия поиска "в глубину" без ограничения;

2) "частичную" унификацию без проверки вхождения переменной4.

Эти конкретизации направлены, прежде всего, на упрощение ПРОЛОГа с точки зрения программирования. К примеру, "частичная" унификация имеет алгоритмическую сложность порядка 0(п), вместо 0(п2) для полной унификации, а стратегия поиска "в глубину" просто реализуется в виде стековой машины. Как следствие, с точки зрения систем АДТ ПРОЛОГ некорректен и неполон (доказуемая терема может быть недоказана).

Исследования в области повышения эффективности реализации этих языков играют важную роль в развитии программных систем АДТ. Существуют реализации машины Уоррена для ЭВМ с разной архитектурой: последовательные и параллельные машины Уоррена. Компилятор ПРОЛОГа транслирует программу в команды машины Уоррена для конкретной архитектуры, создавая таким образом новую реализацию системы АДТ.

3Аббрев. от "Машина Функционального Программирования."

4От англ. occur check — проверка вхождения.

Языки логического программирования получили дальнейшее развитие в направлении совершенствования методов вывода решения. Например, существуют разные системы программирования, соединившие в себе свойства языков ЛИСП и ПРОЛОГ (например, LogLISP Дж. Робинсона). В Иркутске была разработана система программирования FLANG5 [30] (см. также ряд других, в том числе более ранних, работ по логическому программированию в ограничениях: GNU Prolog6, PROLOG-III [31]).

Рассмотренные языки программирования поддерживают автоматическое решение задач на основе АДТ, но не исключают необходимости создания более или менее полномасштабных специализированных систем АДТ (таких, как AURA), специально ориентированных на АДТ, а не на применение в задачах ИИ (когда АДТ оказывается лишь инструментом решения более широкого круга задач в духе дедуктивных построений или автоматизированных рассуждений).

Большинство современных программ АДТ, в зависимости от специфики используемых методов АДТ, можно разделить на следующие группы [6]:

1) синтаксические, или универсальные, не использующие никакой дополнительной информации, кроме синтаксического строения формулы;

2) эвристические, где главную роль играют специальные свойства ее моделей и развиваются на основе систематизации знаний об устройстве предметной области;

3) поиска вывода с равенством.

Среди систем первой группы, т.е. универсальных, наиболее популярными в области ИИ являются системы:

1.1) резолюционного типа, реализующие в разных модификациях метод резолюции [11],

1.2) генценовского типа либо в форме так называемого естественного (натурального) вывода [10], который в сравнении с резолюционным выводом более напоминает манеру рассуждений человека, либо в форме секвенциального вывода [7], в котором секвенции играют роль задач и выводы имеют вид некоторых конечных многошаговых процессов последовательностей декомпозиции задач на подзадачи до получения тривиальных подзадач.

5Аббрев. от Functional-logical programming LANGuage — Язык функционально-логического программирования.

6См. http://www.gnu.org/software/prolog.

Примером системы синтаксической группы является программа OTTER7 [32]. В ее машине вывода реализован ряд разновидностей метода резолюции. Система поддерживает работу с равенством (без привлечения аксиом равенства). Таким образом, OTTER сочетает в себе свойства универсальных систем АДТ и систем третьей группы [6]. Программа реализована на языке "С". Общий алгоритм работы системы можно найти в [33].

В настоящее время АДТ — наиболее формализованное направление автоматизации дедуктивных построений (automated deduction) и автоматизированных рассуждений (automated reasoning) (см. [34]), к которым относятся синтез и верификация аппаратного и программного обеспечения, тестирование и синтез гипотез, построение планов и т.д. В последнее время область автоматизированных рассуждений дополнена новым классом задач на стыке теории автоматического управления и искусственного интеллекта — задач интеллектного управления динамическими системами. Исследования ведутся активно по применению логического вывода (JIB) в задачах управления с целью повышения интеллектуального уровня систем управления [35, 36].

Любое продвижение в совершенствовании методов и программного обеспечения АДТ (логического вывода) является актуальным, так как, как правило, улучшает качество решения перечисленных задач. Переход к более выразительным языкам и более сильным методам дедукции позволяет расширить класс решаемых задач.

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

В [37, 38] предложены языки и исчисления позитивно-образованных формул (по-формул), в определенной мере удовлетворяющие указанным требованиям и принадлежащие первой группе в приведенной выше классификации. Они и составляют теоретическую базу создания программной системы КВАНТ/1 — предмета диссертации.

7Аббрев. от Organized Techniques for Theorem-proving and Research — Организованные методики для доказательства теорем и эффективных исследований.

Заключение

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

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

2. На основе этого алгоритма создана программная система КВАНТ/1 автоматического доказательства теорем, в которой реализованы также дополнительные стратегии выборки "по приоритетам" и "к-опро-вержения". Система КВАНТ/1 переносима на другие программно-аппаратные РОБ 1Х-платформы.

3. Показана полезность разработанного математического обеспечения для решения сложных комбинаторных задач; решена задача о "паровом катке".

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

Перспективными направлениями развития разработанной системы КВАНТ/1 являются программная реализация модификаций исчисления </, ориентированных на обработку динамических знаний, и приложения системы к автоматизации планирования действий.

1. A. Newell, J. С. Shaw. Programming the Logic Theory Machine // 1.: Proceedings of the 1957 Western Joint Computer Conference, IRE, 1957, P. 230-240.

2. A. Newell, J. C. Shaw, H. A. Simon. Empirical Explorations With the Logic Theory Machine // Proceedings of the Western Joint Computer Conference, Vol. 15, 1957, P. 218-239.

3. A. N. Whitehead, B. Russell. Principia Mathematica, Cambridge University Press, Cambridge, 1910.

4. H. Gelernter, J. R. Hanson, D. L. Loveland. Empirical Exploration of the Geometry Theorem Proving Machine // Ibid., Vol. 4, 1960, P. 143-147.

5. H. Gelernter. Realization of a Geometry-Theorem Proving Machine //In: Proceedings of an International Conference on Information Processing, Paris, 1959, P. 273-282.

6. А. А. Воронков, А. И. Дегтярёв. Автоматическое доказательство теорем. I // Кибернетика, N 3, 1986, С. 27-33.

7. Wang Нао. Toward Mechanical Mathematics // IBM J. Res. Devel., Vol. 4, No 1, 1960, P. 2-22.

8. С. Ю. Маслов. Обратный метод установления выводимости в классическом исчислении предикатов // ДАН СССР, Т. 159, N 1, 1964, С. 17-20.

9. Н. А. Шанин, Г. В. Давыдов и др. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний, JL: Наука, 1965.

10. J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle // Journal of the ACM, No 12, 1965, P. 23-41.

11. Г. В. Давыдов. Синтез метода резолюции с обратным методом // Сб. Зап. научн. семинаров ЛОМИ АН СССР, Т. 20, JL: Наука, 1971.

12. JI. Воз. Решение некоторых открытых проблем с помошью программы для автоматического доказательства теорем // Сб. Кибернетический сборник. Новая серия. Вып. 21, М.: Мир, 1984, С. 235-263.

13. С. Н. Васильев, В. М. Матросов. Принцип сравнения в математической теории систем // Сб. Тез. докл. V Казахстанской научной конференции по математике и механике, Алма-Ата, Ч. I, 1974, С. 34-36.

14. В. М. Матросов, С. Н. Васильев, В. Г. Каратуев и др. Алгоритмы вывода теорем метода ВФЛ, Новосибирск: Наука, 1981.

15. S. N. Vassilyev. Machine Synthesis of Mathematical Theorems // J. of Logic Programming, Vol. 9, No 2&3, 1990, P. 235-266.

16. В. И. Мартьянов. О методах задания и частичного построения теорий на ЭВМ // Кибернетика, N 6, 1982, С. 102-110.

17. V. I. Martyanov, V. М. Matrosov, S. N. Vassilyev. Computer Method of Theorem Synthesis and Proving // In: Abstracts of International Congress on Logic, Methodology and Philosophy of Science, Vol. 1, 1987.

18. IH. Б. Гулямов. Математическое и программное обеспечение решения первопорядковых логических уравнений, канд. дисс., ИрВЦ СО РАН, Иркутск, 1997.

19. С. Н. Васильев, А. К. Жерлов, Ш. Б. Гулямов, Ю. Ф. Литвинов. О логических средствах системы планирования ПАСАД // Сб. Алгоритмы, вып. 66, Ташкент, АН УзССР, 1988, С. 97-112.93

20. S. A. Butyrin, V. P. Makarov, R. R. Mukumov, Ye. Somov, S. N. Vassilyev. An Expert System for Design of Spacecraft Attitude Control System // Artificial Intelligence in Engineering, Vol. 11, No 1, 1997, P. 49-59.

21. A. Church. The Calculi of Lambda Conversion, Princeton University Press, 1941.

22. J. McCarthy, P.W. Abrahams, D.J. Edwards, T.P. Hart, M.I. Levin. LISP 1.5 Programmers Manual, MIT Press, 1962.

23. A. Colmerauer. Les systems-Q on un Formalisme pour Analyser et Synthetiser des Phrases sur Qrdinateur // In: Publication Interne, No 43, Dept. d'Informatique. Universite de Montreal, 1973.

24. R. Kowalski. Predicate Logic as a Programming Language // In: Proceedings of the IFIP-74 Congress, Elsevier Publ., 1974, P. 569-574.

25. D. Warren. Implementing PROLOG — Compiling Logic Programs. 1 and 2 // In: D.A.I. Research Report, Vol. 40, 1977.

26. M. Бранохе. Управление памятью в реализациях ПРОЛОГА // Сб. Логическое программирование, М.: Мир, 1988, С. 193-210.

27. C.-L. Chang, R.C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, San Francisco, London, 1973.

28. A. Mantzivoda. Flang: A Functional-Logic Language // In: Lect. Notes in Comp. Sei. (H. Boley, M. M. Richter, eds.), Vol. 567, Splingler, 1992, P. 257-270.

29. A. Colmerauer. An Introduction to Prolog III // Communications of the ACM, Vol. 33, No 7, 1990.

30. W. W. McCune. Otter 2.0 Users Guide. Tech. Rept. Mathematics and Computer Science Division, Argonne, 111., 1990.

31. S. J. Russel, P. Norvig. Artificial Intelligence: A Modern Approach, Prentice Hall, Inc., Upper Saddle River, New Jersey, 1995.

32. L. Wos, R. Overbeek, E. Lusk, J. Boyle. Automated Reasoning: Introduction and Applications, McGraw-Hill, New York, 1992.

33. S. N. Vassilyev, A. K. Zherlov. Логическое моделирование и управление в реальном времени // Сб. Интеллектуальные системы в машиностроении (под ред. В. А. Виттиха), Т. 2, Самарский филиал Института машиноведения РАН, Самара, 1991, С. 33-38.

34. D. М. Gabbay, М. Reynolds. Towards a Computational Treatment of Time // In: Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4, "Epistemic and Temporal Reasoning", Clarendon Press, Oxford, 1995, P. 351-437.

35. С. H. Васильев, А. К. Жерлов. Об исчислении типово-кванторных формул // Докл. Акад. Наук, Т. 343, N 5, 1995, С. 583-585.

36. С. Н. Васильев. Метод синтеза условий выводимости хорновских и некоторых других формул / / Сибирский математический журнал, Т. 38, N 5, 1997, С. 1034-1046.

37. S. N. Vassilyev. Modeling Logical Derivation and Hypothesis Generation // In: Proc. of CESA'96 Conference, Vol. 1, 1996, P. 148153.

38. E. Cherkashin, A. Postoenko, S. Vassilyev, A. Zherlov. New Logics for Intelligent Control // In: Proc. of International Conference of Florida Artificial Intelligence Research Society, 1999.

39. С. К. Клини. Введение в метаматематику, М.: ИЛ, 1957.

40. Ch. Walter. A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution // In: Proc. of the National Conf on AI, 1984, P. 330334.

41. С. H. Васильев, E. А. Черкашин. Представление и обработка знаний в языке поя-формул // Сб. Оптимизация, Управление, Интеллект, N 2, Издательство ИрВЦ СО РАН, Иркутск, 1997, С. 156-176.

42. Е. Cherkashin, S. Vassilyev. On Intelligent Guidance of Telescope // In: Proc. of Computational Engineering in System Application International Conference, Vol. 2, 1998, P. 195-200.

43. E. Cherkashin, S. Vassilyev. Telescope Guidance to the Center of a Planet via ATP: Method and Software // In: Nonlinear Probelms in Aviation and Aerospace (S. Sivasundaram, ed.), Vol. 1, 1998, P. 147-155.

44. С. Н. Васильев, Е. А. Черкашин. Интеллектное управление телескопом // Сибирский журнал индустриальной математики, Т. 1, N 2, 1998, С. 81-98.

45. Е. A. Cherkashin, S. N. Vassilyev. Telescope Guidance via Automatic Theorem proving // In: Proc. of International Conference on System, Man, and Cybernetics, 1998, P. 1439-1444.

46. E. А. Черкашин, С. H. Васильев. Временной вывод в интеллектном управлении телескопом // Сб. Третий Международный симпозиум "Интеллектуальные системы1998, С. 70-75.

47. Е. Cherkasin, S. Vassilyev. Intelligent Control of Moving Objects // In: Mini-Micro Systems, Numerical Simulation and its Software, Vol. 19, 1998, P. 4-24.

48. P. Андерсон. Доказательство правильности программ, М.: Мир, 1982.

49. Т. Бадд. Объектно-ориентированное программирование в действии, Спб.: Питер, 1997.

50. Т. Чан. Системное программирование на С++ для UNIX, Киев: Издательская группа BHV, 1997.

51. JI. Бек. Введение в системное программирование, М.: Мир, 1988.

52. А. К. Жерлов. Логическое исчисление позитивно-образованных формул, его свойства и применение, канд. дисс., ИДСТУ СО РАН, Иркутск, 1999.

53. Г. Г. Бильченко, С. Н. Васильев, В. М. Матросов. Система наведения телескопа на центр планеты в неполной фазе // Сб. Труды V Международного симпозиума ИФАК по автоматическому управлению в пространстве, Т. 1, М.: Наука, 1975, С. 45-57.

54. Р. С. Эстей. Прибор для слежения за Землей или Луной, находящейся в неполной фазе // Сб. Автоматическое управление космическими летательными аппаратами, М.: Наука, 1968.

55. С. Green. The Application of Theorem Proving to Question Answering Systems, Ph.D. diss., Stanford University, Stanford, California, 1969.1. Список процедур

56. Поиск ответной подстановки.292 Унификация .31

57. Преобразование базовой подформулы в ходе шага вывода . . 38

58. Шага вывода в корне дерева .41

59. Поиск опровержения по-формулы.42