Специальный семинар "Автоматическое доказательство теорем".
Осенний семестр 2006/07 и 2007/08 уч. г.

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

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

Доклады

  1. Синтаксис и семантика языка логики предикатов.
  2. Исчисление гильбертовского типа.
  3. Техника естественного вывода.
  4. Секвенциальное исчисление генценовского типа. Минус-нормализация вывода. Метод метапеременных.
  5. Унификация.
  6. Метод семантических таблиц.
  7. Нормальные формы (конъюнктивная, предваренная, скулемовская).
  8. Теорема Эрбрана.
  9. Метод резолюций.
  10. Обратный метод Маслова.
  11. Применение логики предикатов для представления знаний.