Преподаватель Герасимов Александр Сергеевич
Классическая двузначная логика предикатов достаточно выразительна для представления многих знаний. Для получения заключений на основе имеющихся знаний применяются системы автоматического поиска доказательства (автопруверы).
В спецкурсе будет сделано напоминание о синтаксисе и семантике языка логики предикатов и освещено несколько основополагающих методов поиска доказательства для логики предикатов. В рамках спецсеминара планируется разработать автопрувер (что будет отличной практикой программирования) и рассмотреть разделы, дополняющие спецкурс.
Спецкурс и спецсеминар официально предназначены для студентов 341-342 групп, но также приглашаются все желающие.
Основные вопросы, которые планируется изучить в рамках спецкурса
Язык логики предикатов и его семантика: язык первого порядка, интерпретация языка первого порядка, общезначимые формулы, логическое следствие, теорема о логическом следствии, равносильные формулы.
Общее понятие исчисления.
Исчисление предикатов гильбертовского типа: формулировка исчисления, корректность и полнота исчисления, техника естественного вывода, алгоритм Британского музея.
Секвенциальное исчисление предикатов генценовского типа: систематический поиск контрпримера для формулы, формулировка секвенциального исчисления предикатов, корректность секвенциального исчисления предикатов, полнота секвенциального исчисления высказываний, метод метапеременных, схема алгоритма поиска вывода в секвенциальном исчислении предикатов, теорема о полноте секвенциального исчисления предикатов и о корректности такого алгоритма; соотношение секвенциального исчисления предикатов и исчисления предикатов гильбертовского типа, допустимость правила сечения.
Унификация: подстановки, унификаторы, наиболее общие унификаторы, алгоритм унификации и теорема о его корректности. Унификация при поиске вывода в секвенциальном исчислении предикатов с метапеременными.
Метод резолюций: метод резолюций для логики высказываний, теорема о его корректности; cкулемовская стандартная форма, теорема о выполнимости формулы и её скулемовской стандартной формы; метод резолюций для логики предикатов, его корректность; эрбрановские интерпретации, теорема о ложности множества дизъюнктов в эрбрановских интерпретациях; семантические деревья, теорема Эрбрана в терминах семантических деревьев и в терминах основных примеров дизъюнктов, основанный на теореме Эрбрана алгоритм проверки невыполнимости множества дизъюнктов; лемма подъёма, теорема о полноте метода резолюций для логики предикатов, алгоритм доказательства методом резолюций.
Основы логического программирования: логическая программа и её декларативная семантика, SLD-резолюция, пример представления знаний в виде логической программы и поиска ответа на запрос к логической программе, операционная семантика логической программы, теорема о корректности вычисленной подстановки.
Темы возможных докладов на спецсеминаре
Алгоритм унификации Мартелли-Монтанари.
Martelli A. and Montanari U. An efficient unification algorithm. // ACM Transactions on Programming Languages and Systems, Vol. 4, Issue 2 (1982), pp. 258-282. http://www.nsl.com/misc/papers/martelli-montanari.pdf
Свойства наиболее общих унификаторов.
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 (полный текст доступен с компьютеров СПбГУ)
Метод семантических таблиц. Ослабление ограничений на кванторные правила вывода в методе семантических таблиц с метапеременными.
Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996. http://link.springer.com/book/10.1007/978-1-4612-2360-3/page/1 (полный текст доступен с компьютеров СПбГУ)
Метод подъёма решений при поиске вывода в секвенциальном исчислении с метапеременными.
Б.Ю. Конев, Т. Жебелиан. Метод подъёма решений для работы с метапеременными в системе Theorema. // Записки научных семинаров ПОМИ, том 293 (2002). ftp://ftp.pdmi.ras.ru/pub/publicat/znsl/v293/p094.ps.gz
Равенство в секвенциальных исчислениях.
A. Degtyarev and A. Voronkov. Equality Reasoning in Sequent-Based Calculi. In: Handbook of Automated Reasoning. Volume I. Editors A. Robinson and A. Voronkov. Elsevier Science, 2001. http://www.dcs.kcl.ac.uk/staff/anatoli/papers/hand_eq_seq.ps
Семантическая резолюция и лок-резолюция.
Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 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