Прикладная логика
(Логические основы программирования)

I.Логическое программирование

1. Логические программы
2. Унификация. Алгоритм унификации, теорема об унификации.
3. Резолюции. Вывод. Теорема о корректности.
4. Интерпретации Эрбрана. Теорема о наименьшей модели Эрбрана.
5. Теорема о множестве решений программы. Теорема о полноте резолюций.
6. Вычислимость частично рекурсивных функций с помощью логических программ. Алгоритмические свойства наименьшей модели Эрбрана.
7. Проблема отрицания. Правило CWA.
8. Отрицание как неуспех. Характеризация финитно неуспешного множества.
9. Пополнение программ. Соотношение различных правил для отрицания.

II.Темпоральная логика программ

1. Язык и семантика темпоральной логики программ: пропозициональная часть. Основные эквивалентности.
2. Темпоральное пропозициональное исчисление. Теорема о корректности.
3. Теорема о дедукции в S_TA. Теорема о замене.
4. Отсутствие сильной теоремы о полноте исчисления S_TA.
5. Пополнения данного множества формул. Леммы о пополнениях. Дерево Т(F). Свойства полных путей и их существование. Теорема о существовании модели. Теорема о полноте пропозиционального исчисления.
6. Язык и семантика темпоральной логики предикатов.
7. Темпоральное исчисление предикатов. Теорема о корректности.

III.Динамическая логика

1. Пропозициональная динамическая логика. Язык и семантика.
2. Аксиоматизация пропозициональной динамической логики. Теорема о корректности. Полнота и разрешимость ПДЛ.
3. Компактность и проблема следования.
4. Детерминистская ПДЛ. Погружение темпоральной логики в ДПДЛ.

   ---

   Литература

   1. J.W.Lloyd. Foundations of Logic Programming, 2nd Ed. Springer-Verlag, 1987.
   2. F.Kroeger. Temporal logic of programs. Springer, 1987.
   3. D.Harel. First-order dynamic Logic. Springer, Berlin, 1979.

   Профессор Л.Л.Максимова