Герасимов А.С. Курс математической логики и теории вычислимости

Учебное пособие, издание третье, исправленное и дополненное. — СПб.: Лема, 2011. — 284 с.Настоящее учебное пособие предназначено для изучения математической логики и теории алгоритмов. В нём описаны языки логики высказываний и логики предикатов первого порядка, семантика этих языков. На основе общего понятия исчисления изложены исчисления гильбертовского типа, секвенциальные исчисления и метод резолюций как способы формального математического доказательства. Рассмотрены основные формальные аксиоматические теории — элементарная арифметика и теория множеств Цермело-Френкеля. Теория алгоритм в представлена теорией вычислимости, в рамках которой дано несколько точн х определений понятия алгоритма и доказана неразрешимость некоторых проблем.
Дополнительная глава посвящена исчислению для формального доказательства правильности программ некоторого императивного языка программирования. В данной книге имеется более 190 упражнений.
Это учебное пособие адресовано в первую очередь студентам, специализирующимся по информатике, но будет полезно студентам разных математических специальностей (направлений подготовки), а также всем желающим начать систематическое изучение математической логики.Исчисления высказываний
Исчисления предикатов
Формальные аксиоматические теории
Метод резолюций для логики предикатов
Теория вычислимости
Исчисление Хоара для доказательства корректности
программ
Приложение. Свойства секвенциального исчисления преди-
катов и формальные аксиоматические теории на его основе