Практические занятия по дисциплине
"Структуры и алгоритмы компьютерной обработки данных"
для студентов, обучающихся специальности
"Математическое обеспечение и администрирование информационных систем".
Весенний семестр 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а.