Специальный курс
"Введение в автоматическое доказательство теорем" и
специальный семинар
"Автоматическое доказательство теорем"
для студентов, обучающихся по направлению
"Математическое обеспечение и администрирование информационных систем".
Осенний семестр 2013/14 уч. г.
Классическая двузначная логика предикатов достаточно выразительна для
представления многих знаний. Для получения заключений на основе имеющихся
знаний применяются системы автоматического поиска доказательства (автопруверы).
В спецкурсе будет сделано напоминание о синтаксисе и семантике языка логики
предикатов и освещено несколько основополагающих методов поиска доказательства
для логики предикатов. В рамках спецсеминара планируется разработать автопрувер
(что будет отличной практикой программирования) и рассмотреть разделы,
дополняющие спецкурс.
Спецкурс и спецсеминар официально предназначены для студентов 341-342 групп,
но также приглашаются все желающие.
Основные вопросы, которые планируется изучить в рамках спецкурса
- Язык логики предикатов и его семантика:
язык первого порядка, интерпретация языка первого порядка,
общезначимые формулы, логическое следствие, теорема о логическом следствии,
равносильные формулы.
- Общее понятие исчисления.
- Исчисление предикатов гильбертовского типа:
формулировка исчисления, корректность и полнота исчисления,
техника естественного вывода, алгоритм Британского музея.
- Секвенциальное исчисление предикатов генценовского типа:
систематический поиск контрпримера для формулы,
формулировка секвенциального исчисления предикатов,
корректность секвенциального исчисления предикатов,
полнота секвенциального исчисления высказываний,
метод метапеременных,
схема алгоритма поиска вывода в секвенциальном исчислении предикатов,
теорема о полноте секвенциального исчисления предикатов и о корректности
такого алгоритма;
соотношение секвенциального исчисления предикатов
и исчисления предикатов гильбертовского типа, допустимость правила сечения.
- Унификация: подстановки, унификаторы, наиболее общие унификаторы,
алгоритм унификации и теорема о его корректности.
Унификация при поиске вывода в секвенциальном исчислении предикатов
с метапеременными.
- Метод резолюций:
метод резолюций для логики высказываний, теорема о его корректности;
cкулемовская стандартная форма,
теорема о выполнимости формулы и её скулемовской стандартной формы;
метод резолюций для логики предикатов, его корректность;
эрбрановские интерпретации,
теорема о ложности множества дизъюнктов в эрбрановских интерпретациях;
семантические деревья, теорема Эрбрана в терминах семантических деревьев и
в терминах основных примеров дизъюнктов,
основанный на теореме Эрбрана алгоритм проверки невыполнимости множества
дизъюнктов;
лемма подъёма, теорема о полноте метода резолюций для логики предикатов,
алгоритм доказательства методом резолюций.
- Основы логического программирования:
логическая программа и её декларативная семантика,
SLD-резолюция,
пример представления знаний в виде логической программы и
поиска ответа на запрос к логической программе,
операционная семантика логической программы,
теорема о корректности вычисленной подстановки.
Темы возможных докладов на спецсеминаре
-
Алгоритм унификации Мартелли-Монтанари.
-
Свойства наиболее общих унификаторов.
-
Метод семантических таблиц. Ослабление ограничений на кванторные правила вывода
в методе семантических таблиц с метапеременными.
-
Метод подъёма решений при поиске вывода в секвенциальном исчислении с
метапеременными.
-
Равенство в секвенциальных исчислениях.
-
Семантическая резолюция и лок-резолюция.
-
Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.
М.: Наука, 1983. (Глава 6.)
-
Линейная резолюция.
-
Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.
М.: Наука, 1983. (Глава 7.)
-
Резолюция с равенством.
-
Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.
М.: Наука, 1983. (Глава 8.)
-
Обратный метод Маслова.
-
Оревков В.П. Обратный метод поиска вывода.
В книге: Адаменко А.Н., Кучуков А.М. Логическое программирование и
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