Специальный семинар "Автоматическое доказательство теорем".

Осенний семестр 2006/07 и 2007/08 уч. г.

Преподаватель Герасимов Александр Сергеевич

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

Доклады

• 1. Синтаксис и семантика языка логики предикатов.

     1. • Колмогоров А.Н., Драгалин А.Г. Введение в математическую логику. (Глава II, параграфы 1-5: 1, 2, 4 и 5 обзорно, 3 подробно.)

  2. Исчисление гильбертовского типа.

     1. • Колмогоров А.Н., Драгалин А.Г. Введение в математическую логику. (Глава III, параграф 1.)

  3. Техника естественного вывода.

     1. • Колмогоров А.Н., Драгалин А.Г. Введение в математическую логику. (Глава III, параграф 2.)

        • [для ознакомления, необязательно для доклада] Генцен Г. Исследования логических выводов. (Раздел II.) В книге: Математическая теория логического вывода. - М.: Наука, 1967.

  4. Секвенциальное исчисление генценовского типа. Минус-нормализация вывода. Метод метапеременных.

     1. • Колмогоров А.Н., Драгалин А.Г. Математическая логика. Дополнительные главы. (Глава III, параграф 3.)

        • Кангер С. Упрощенный метод доказательства для элементарной логики. В книге: Математическая теория логического вывода. - М.: Наука, 1967. С. 200-207.

        • Маслов С.Ю., Минц Г.Е. Теория поиска вывода и обратный метод. (Разделы 2.4, 2.5). В книге: Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983.

  5. Унификация.

     1. • Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. (Параграфы 5.3 и 5.4.)

  6. Метод семантических таблиц.

     1. • Hahnle R. Tableaux and Related Methods. (Разделы 3.1-3.4 и лишь необходимые определения из раздела 2.) In: Handbook of Automated Reasoning. Volume I. Editors Robinson A., Voronkov A. Elsevier Science, 2001. http://www.cs.chalmers.se/~reiner/papers/03.ps.gz

        • Бет Э. Метод семантических таблиц. В книге: Математическая теория логического вывода. - М.: Наука, 1967. С. 191-199.

  7. Нормальные формы (конъюнктивная, предваренная, скулемовская).

     1. • Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. (Параграфы 2.4, 3.3 и 4.2.)

  8. Теорема Эрбрана.

     1. • Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. (Параграфы 4.3-4.5.)

  9. Метод резолюций.

     1. • Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. (Параграфы 5.2, 5.5 и 5.6.)

  10. Обратный метод Маслова.

      1. • Маслов С.Ю., Минц Г.Е. Теория поиска вывода и обратный метод. (Параграфы 3 и 4.) В книге: Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983.

         • [для ознакомления, необязательно для доклада] Маслов С.Ю. Обратный метод установления выводимости для логических исчислений. // Труды Матем. ин-та АН СССР им. В.А. Стеклова. Том 98. М.: Наука, 1968. С. 26-87.

  11. Применение логики предикатов для представления знаний.

      1. • Рассел С., Норвиг П. Искусственный интеллект: современный подход, 2-е изд. М.: Издательский дом "Вильямс", 2006. (Главы 8, 10.)