Прикладная логика
(Логические основы программирования)
I.Логическое программирование
- Логические программы
- Унификация. Алгоритм унификации, теорема об унификации.
- Резолюции. Вывод. Теорема о корректности.
- Интерпретации Эрбрана. Теорема о наименьшей модели Эрбрана.
- Теорема о множестве решений программы. Теорема о полноте
резолюций.
- Вычислимость частично рекурсивных функций с помощью
логических программ. Алгоритмические свойства наименьшей
модели Эрбрана.
- Проблема отрицания. Правило CWA.
- Отрицание как неуспех. Характеризация финитно неуспешного
множества.
- Пополнение программ. Соотношение различных правил для
отрицания.
II.Темпоральная логика программ
- Язык и семантика темпоральной логики программ:
пропозициональная часть. Основные эквивалентности.
- Темпоральное пропозициональное исчисление. Теорема о
корректности.
- Теорема о дедукции в STA. Теорема о замене.
- Отсутствие сильной теоремы о полноте исчисления STA.
- Пополнения данного множества формул. Леммы о пополнениях.
Дерево Т(F). Свойства полных путей и их существование.
Теорема о существовании модели. Теорема о полноте
пропозиционального исчисления.
- Язык и семантика темпоральной логики предикатов.
- Темпоральное исчисление предикатов. Теорема о корректности.
III.Динамическая логика
- Пропозициональная динамическая логика. Язык и семантика.
- Аксиоматизация пропозициональной динамической логики.
Теорема о корректности. Полнота и разрешимость ПДЛ.
- Компактность и проблема следования.
- Детерминистская ПДЛ. Погружение темпоральной логики в ДПДЛ.
Литература
- J.W.Lloyd. Foundations of Logic Programming, 2nd Ed.
Springer-Verlag, 1987.
- F.Kroeger. Temporal logic of programs. Springer, 1987.
- D.Harel. First-order dynamic Logic. Springer, Berlin, 1979.
Профессор Л.Л.Максимова