Специальный курс "Введение в автоматическое доказательство теорем" и
специальный семинар "Автоматическое доказательство теорем"
для студентов, обучающихся по направлению "Математическое обеспечение и администрирование информационных систем".
Осенний семестр 2013/14 уч. г.



Классическая двузначная логика предикатов достаточно выразительна для представления многих знаний. Для получения заключений на основе имеющихся знаний применяются системы автоматического поиска доказательства (автопруверы).

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

Спецкурс и спецсеминар официально предназначены для студентов 341-342 групп, но также приглашаются все желающие.


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

  • Язык логики предикатов и его семантика: язык первого порядка, интерпретация языка первого порядка, общезначимые формулы, логическое следствие, теорема о логическом следствии, равносильные формулы.
  • Общее понятие исчисления.
  • Исчисление предикатов гильбертовского типа: формулировка исчисления, корректность и полнота исчисления, техника естественного вывода, алгоритм Британского музея.
  • Секвенциальное исчисление предикатов генценовского типа: систематический поиск контрпримера для формулы, формулировка секвенциального исчисления предикатов, корректность секвенциального исчисления предикатов, полнота секвенциального исчисления высказываний, метод метапеременных, схема алгоритма поиска вывода в секвенциальном исчислении предикатов, теорема о полноте секвенциального исчисления предикатов и о корректности такого алгоритма; соотношение секвенциального исчисления предикатов и исчисления предикатов гильбертовского типа, допустимость правила сечения.
  • Унификация: подстановки, унификаторы, наиболее общие унификаторы, алгоритм унификации и теорема о его корректности. Унификация при поиске вывода в секвенциальном исчислении предикатов с метапеременными.
  • Метод резолюций: метод резолюций для логики высказываний, теорема о его корректности; cкулемовская стандартная форма, теорема о выполнимости формулы и её скулемовской стандартной формы; метод резолюций для логики предикатов, его корректность; эрбрановские интерпретации, теорема о ложности множества дизъюнктов в эрбрановских интерпретациях; семантические деревья, теорема Эрбрана в терминах семантических деревьев и в терминах основных примеров дизъюнктов, основанный на теореме Эрбрана алгоритм проверки невыполнимости множества дизъюнктов; лемма подъёма, теорема о полноте метода резолюций для логики предикатов, алгоритм доказательства методом резолюций.
  • Основы логического программирования: логическая программа и её декларативная семантика, SLD-резолюция, пример представления знаний в виде логической программы и поиска ответа на запрос к логической программе, операционная семантика логической программы, теорема о корректности вычисленной подстановки.

Темы возможных докладов на спецсеминаре

  1. Алгоритм унификации Мартелли-Монтанари.
  2. Свойства наиболее общих унификаторов.
    • Lassez J.-L., Maher M., Marriott K. Unification Revisited. // Lecture Notes in Computer Science, Vol. 306 (1988), pp. 67-113. http://www.springerlink.com/content/f4657x51544h1211 (полный текст доступен с компьютеров СПбГУ)
  3. Метод семантических таблиц. Ослабление ограничений на кванторные правила вывода в методе семантических таблиц с метапеременными.
  4. Метод подъёма решений при поиске вывода в секвенциальном исчислении с метапеременными.
    • Б.Ю. Конев, Т. Жебелиан. Метод подъёма решений для работы с метапеременными в системе Theorema. // Записки научных семинаров ПОМИ, том 293 (2002). ftp://ftp.pdmi.ras.ru/pub/publicat/znsl/v293/p094.ps.gz
  5. Равенство в секвенциальных исчислениях.
  6. Семантическая резолюция и лок-резолюция.
    • Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. (Глава 6.)
  7. Линейная резолюция.
    • Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. (Глава 7.)
  8. Резолюция с равенством.
    • Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. (Глава 8.)
  9. Обратный метод Маслова.
    • Оревков В.П. Обратный метод поиска вывода. В книге: Адаменко А.Н., Кучуков А.М. Логическое программирование и Visual Prolog. СПб.: БХВ-Петербург, 2003.

Для тестирования и отладки автопрувера предлагается использовать формулы без предикатного символа равенства из следующей статьи:
    Pelletier F. J. Seventy-Five Problems for Testing Automatic Theorem Provers. // Journal of Automated Reasoning, 2 (1986), pp. 191-216. http://www.sfu.ca/~jeffpell/papers/75ATPproblems86.pdf
    Список опечаток к предыдущей статье: Pelletier F. J. Errata. // Journal of Automated Reasoning, 4 (1988), pp. 235-236. http://www.sfu.ca/~jeffpell/papers/75ProblemsErrata.pdf
    Исправление ещё одной опечатки: Pelletier F. J., Sutcliffe G. An Erratum for Some Errata to ATP Problems. // Journal of Automated Reasoning, 18 (1997), p. 135. http://www.sfu.ca/~jeffpell/papers/Erratum.ps

Экзаменационные вопросы