Реферат: Математическая логика Лектор 2010/11 уч года: к ф-м наук Носов В. А. Аннотация

Математическая логика


Лектор 2010/11 уч. года: к. ф-м наук Носов В.А.


Аннотация


Курс предназначен для студентов и аспирантов, специализирующихся в области вычислительных наук. Его целью является ознакомление слушателей с некоторыми разделами математической логики, оказывающими наибольшее влияние на теорию и практику современного программирования. К их числу относится классическая логика предикатов как формальный язык представления знаний, аппарат логического вывода как метод дедуктивного извлечения знаний, метод резолюций как наиболее распространенный подход к автоматическому доказательству теорем.

В курсе представлены основы теории логического программирования и принципы реализации логических программ. Рассматриваются также неклассические (модальные, темпоральные, динамические и др.) логики, используемые для представления знаний, спецификации и анализа поведения программ. Большинство рассматриваемых понятий и результатов получают при этом естественное содержательное истолкование в терминах современного программирования.


^ Содержание курса


Логика предикатов первого порядка. Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношение выполнимости формулы на интерпретации. Выполнимость, общезначимость, противоречивость. Модель. Логическое следствие. Семантические таблицы в логике предикатов. Табличный вывод. Теоремы корректности и полноты табличного вывода. Теорема Лёвенгейма-Скулема. Теорема компактности.

^ Метод резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Скулемовская стандартная форма. Эр-брановский универсум, эрбрановский базис, эрбрановские интерпретации. Теорема об эрбрановской модели. Семантические деревья как способ представления эрбрановских интерпретаций. Лемма о семантическом дереве. Теорема Эрбрана. Подстановки. Унификаторы. Алгоритм унификации. Метод резолюций для логики предикатов. Теоремы корректности и полноты резолютивного вывода. Общая схема доказательства общезначимости методом резолюций.

^ Основы логического программирования. Вычислительные возможности резолютивного вывода. Хорновские дизъюнкты. Синтаксис языка логического программирования: логические программы и запросы. Теорема о наименьшей эрбрановской модели для логической программы. Декларативная семантика логических программ. Правильный ответ. Оператор непосредственного следования и его неподвижные точки. Денотационная семантика логических программ. Теорема о структуре наименьшей эрбрановской модели. SLD-peзолюция. SLD-резолютивные вычисления (опровержения) логических программ. Вычислимый ответ. Множество успехов. Операционная (процедурная) семантика логических программ. Теоремы корректности и полноты SLD-peзолютивных вычислений логических программ. Правило вычислений и его роль. Дерево SLD-вычислений логических программ. Стратегии вычислений. Управление исполнением логических программ. Оператор отсечения и его операционная семантика. Отрицание в Прологе и его семантика. Встроенные предикаты и функции и их операционная семантика. Теорема о вычислительной универсальности чистого Пролога. Теорема Чёрча о неразрешимости логики предикатов первого порядка.

^ Неклассические прикладные логики. Интуиционистская логика высказываний. Модели Крипке интуиционистской логики высказываний. Модальные логики высказываний. Модели Крипке модальной логики высказываний. Темпоральные логики высказываний линейного времени (PLTL) и вычислительных деревьев (CTL): их синтаксис и семантика. Применение темпоральных логик для спецификации и анализа поведения реагирующих систем. Пропозициональная динамическая логика PDL: ее синтаксис и семантика.


Литература


1. Клини С. Математическая логика. М.: Мир. 1973.

2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Мир. 1983.

3. Lloyd J.W. Foundation of Logic Programming. Springer-Verlag. 1984.

4. Apt K.R. From Logic Programming to Prolog. Prentice Hall. 1997.

5. Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. М.: Физматлит. 1995.

6. Метакидес Г., Нероуд А. Принципы логики и логического программирования. М.: Факториал. 1998.


Дополнительная литература


1. Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.: Мир. 1998.

2. Братко И. Программирование на Прологе для искусственного интеллекта. М.: Мир. 1990.

3. Набебин А.А. Логика и Пролог в дискретной математике. М.: Изд-во МЭИ. 1997.

4. Мендельсон Э. Введение в математическую логику. М.: Наука. 1984.

5. Хоггер К. Введение в логическое программирование. М.: Мир. 1988.

6. Клоксин У, Меллиш К. Программирование на языке Пролог. М.: Мир. 1987.

7. Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. М.: Радио и связь. 1987.

8. Стерлинг Л., Шапиро Э. Искусство программирования на языке ПРОЛОГ. М.: Мир. 1990.

9. Янсон А. Турбо-ПРОЛОГ в сжатом изложении. М.: Мир. 1991.

10. Ковальский Р. Логика в решении проблем. М.: Наука. 1990.

11. ЛихтарниковЛ.М., Сукачева Т.Г. Математическая логика. М.: Лань. 1999.