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

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

Задача: реализовать автопрувер для секвенциального
исчисления предикатов генценовского типа (программу,
выводящую формулы в этом исчислении).

Подзадачи:

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

Грамматика (форма Бэкуса-Наура), задающая формулы и учитывающая приоритет
связок:
Формула ::= ЧленЭквивалентнсти {"<=>" ЧленЭквивалентнсти}
ЧленЭквивалентнсти ::= ЧленИмпликации {"=>" ЧленИмпликации}
ЧленИмпликации ::= ЧленДизъюнкции {"|" ЧленДизъюнкции}
ЧленДизъюнкции ::= ЧленКонъюнкции {"&" ЧленКонъюнкции}
ЧленКонъюнкции ::= "~" ЧленКонъюнкции | "(" Формула ")" | АтомарнаяФормула
АтомарнаяФормула ::= ИстинностнаяКонстанта | ПропозициональнаяПеременная
ИстинностнаяКонстанта ::= "F" | "T"

Иерархия классов, представляющих узлы синтаксического дерева формулы исчисления
высказываний:
Формула                                Formula
    АтомарнаяФормула                       AtomicFormula
        ИстинностнаяКонстанта                  TruthConstant
        ПропозициональнаяПеременная            PropositionalVariable
    ФормулаСоСвязкой                       ConnectiveFormula

Рекомендуемая литература по синтаксическому анализу:
Ахо А., Сети Р., Ульман Дж. Компиляторы: принципы, технологии и инструменты.
Пер. с англ. - М.: Издательский дом "Вильямс", 2001.

2. То же, что и в предыдущей подзадаче, но для формулы исчисления предикатов.

Грамматика, задающая формулы исчисления предикатов, получается из
вышеприведенной путем замены правил для нетерминалов ЧленКонъюнкции и
АтомарнаяФормула на правила
ЧленКонъюнкции ::= "~" ЧленКонъюнкции | "(" Формула ")" | АтомарнаяФормула |
                   Квантор ПредметнаяПеременная ЧленКонъюнкции
АтомарнаяФормула ::= ИстинностнаяКонстанта | ПропозициональнаяПеременная |
                     ПредикатнаяПеременная "(" Терм {"," Терм} ")"
и добавления правил
Терм ::= ПредметнаяПеременная | ПредметнаяКонстанта |
         ФункциональнаяПеременная "(" Терм {"," Терм} ")"

Иерархия классов, представляющих узлы синтаксического дерева формулы исчисления
предикатов:
Формула                                    Formula
    АтомарнаяФормула                           AtomicFormula
        ИстинностнаяКонстанта                      TruthConstant
        ПредикатнаяПеременная                      PredicateVariable
            ПропозициональнаяПеременная                PropositionalVariable
    ФормулаСЛогическимСимволом                 LogicalSymbolFormula
        ФормулаСоСвязкой                           ConnectiveFormula
        КванторнаяФормула                          QuantifierFormula

[ЛогическийСимвол]    [LogicalSymbol]
    Связка                Connective
    Квантор               Quantifier

Терм                            Term
    ПредметнаяПеременная            IndividualVariable
    ФункциональнаяПеременная        FunctionalVariable
        ПредметнаяКонстанта             IndividualConstant

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

3а. Тестирование и отладка пропозиционального автопрувера.
В качестве тестов используются пропозициональные формулы из следующей статьи
(полный текст которой доступен с компьютеров СПбГУ):
Pelletier F. J. Seventy-Five Problems for Testing Automatic Theorem Provers.
Journal of Automated Reasoning 2 (1986), pp. 191-216.
http://www.springerlink.com/content/r10030507w282122
Список опечаток к предыдущей статье:
Pelletier F. J. Errata. Journal of Automated Reasoning 4 (1988), pp. 235-236.
http://www.springerlink.com/content/np2x52476672m493
Исправление еще одной опечатки:
Pelletier F. J., Sutcliffe G. An Erratum for Some Errata to ATP Problems.
Journal of Automated Reasoning 18 (1997), p. 135.
http://www.springerlink.com/content/k2r355854361265p

4. Вывод в исчислении предикатов: контрприменение правил вывода, введение
метапеременных при контрприменении кванторных правил; попытка унификации
атомарных формул (попытка подбора термов-значений для метапеременных, при
которых полученные секвенции становятся аксиомами и выполняются ограничения
на примененные кванторные правила); при неудачной унификации продолжение
контрприменения правил вывода; попытка унификации и т.д.

4а. Тестирование и отладка предикатного автопрувера.
В качестве тестов используются предикатные формулы без предиката равенства("=")
из статьи, указанной в подзадаче 3а.