Математическая логика Лектор 2010/11 уч года: к ф-м наук Носов В. А. Аннотация
| Вид материала | Документы |
СодержаниеСодержание курса Метод резолюций. Основы логического программирования. Неклассические прикладные логики. |
- Теория вероятностей и математическая статистика Лектор 2010/11 уч года: д ф. м н.,, 41.34kb.
- Анализ Авторы программы: академик Ильин В. А., доцент Леонтьева Т. А. Лектор 2010/11, 60.87kb.
- Аннотация программы учебной дисциплины «Дискретная математика и математическая логика, 55.65kb.
- Математическая логика, 1012.22kb.
- Календарный план учебных занятий по обязательной дисциплине «Математическая логика»,, 39.04kb.
- Рабочая программа по дисциплине в 2-Математическая логика и теория алгоритмов шифр, 316.78kb.
- Программы кандидатского экзамена по специальности 01. 01. 06 "Математическая логика,, 50.44kb.
- Рабочая учебная программа по дисциплине математическая логика, 72.41kb.
- Обыкновенные дифференциальные уравнения Лектор 2010/2011 уч год: доктор физ мат наук,, 51.11kb.
- Уравнения математической физики Лектор 2010/11 уч года д ф. м наук, и о. проф. Косимов, 67.08kb.
Математическая логика
Лектор 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.