СПб: НИУ ИТМО, 2013. — 131 с.
В пособии описывается история возникновения логики как науки. Рассматриваются основные положения логики высказываний и логики предикатов. Обосновываются принципы логического вывода, применяемые в логике предикатов и ее приложениях к искусственному интеллекту и базам знаний. Приводятся примеры применения многозначной логики в моделировании логических схем. Рассматриваются методы решения задач в логике высказываний и логике предикатов. В приложении приводится именной указатель ученых, внесших значительный вклад в развитии логики как науки.
Пособие предназначено для студентов, обучающихся по направлениям 230100 «Информатика и вычислительная техника» и 231000 «Программная инженерия». Содержание.
Введение.
Логика высказываний .
Формулы высказываний.
Импликация на примере дедукции.
Интерпретация логических формул.
Принцип подстановки.
Алгебра логики высказываний.
Законы логики высказываний. Булева алгебра высказываний. Применение булевой алгебры для проверки тождеств. Применение алгебры для вычислений – метод Квайна. Применение алгебры для доказательства общезначимости. Нормальные формулы. SAT-проблема (прямой метод). Приложения булевой алгебры в технике .
Метод Девиса - Патнема (DP).
Решение SAT-проблемы. Проверка формулы на общезначимость .
Применение тавтологий в рассуждениях.
Аксиоматическая теория высказываний.
Схемы аксиом. Правила преобразования тавтологий. Утверждение о полноте теории высказываний. Утверждение о непротиворечивости .
Логический вывод из гипотез.
Прямой метод вывода. Обратный метод логического вывода из гипотез. Применение правил вывода из гипотез c использованием тождественных алгебраических преобразований. Применение DP-метода при выводе из гипотез. Правило резолюции Робинсона .
Выводы. Задачи в логике высказываний. .
Логика предикатов .
Формулы с одноместными предикатами.
Формулы с многоместными предикатами.
Формулы с кванторами.
Законы логики предикатов с кванторами.
Дизъюнктивное расширение области действия кванторов. Конъюнктивное расширение области действия кванторов. Законы для формул со смешанными кванторами .
Нормальные формулы с предикатами.
Теории первого порядка.
Метод резолюций в логике предикатов.
Приложения логики предикатов.
Применение логики в базах данных. Применение логики к программам .
Выводы. Задачи в логике предикатов.
Логическое (сентенциальное) программирование .
Декларативная семантика программ Пролога.
Процедурная семантика программ Пролога.
Выводы.
Прикладная логика .
Схемотехника логических утверждений.
Приложения многозначной логики в моделировании схем.
Временное моделирование цифровых схем. Четырехзначное логическое моделирование .
Тестирование логических схем.
Структурное троичное тестирование цифровых схем. Структурное четырехзначное тестирование. Алгебро-топологические методы синтеза тестов логических схем .
Выводы. .
Заключение.
Вопросы к зачету.
Список литературы.
Именной указатель.
В пособии описывается история возникновения логики как науки. Рассматриваются основные положения логики высказываний и логики предикатов. Обосновываются принципы логического вывода, применяемые в логике предикатов и ее приложениях к искусственному интеллекту и базам знаний. Приводятся примеры применения многозначной логики в моделировании логических схем. Рассматриваются методы решения задач в логике высказываний и логике предикатов. В приложении приводится именной указатель ученых, внесших значительный вклад в развитии логики как науки.
Пособие предназначено для студентов, обучающихся по направлениям 230100 «Информатика и вычислительная техника» и 231000 «Программная инженерия». Содержание.
Введение.
Логика высказываний .
Формулы высказываний.
Импликация на примере дедукции.
Интерпретация логических формул.
Принцип подстановки.
Алгебра логики высказываний.
Законы логики высказываний. Булева алгебра высказываний. Применение булевой алгебры для проверки тождеств. Применение алгебры для вычислений – метод Квайна. Применение алгебры для доказательства общезначимости. Нормальные формулы. SAT-проблема (прямой метод). Приложения булевой алгебры в технике .
Метод Девиса - Патнема (DP).
Решение SAT-проблемы. Проверка формулы на общезначимость .
Применение тавтологий в рассуждениях.
Аксиоматическая теория высказываний.
Схемы аксиом. Правила преобразования тавтологий. Утверждение о полноте теории высказываний. Утверждение о непротиворечивости .
Логический вывод из гипотез.
Прямой метод вывода. Обратный метод логического вывода из гипотез. Применение правил вывода из гипотез c использованием тождественных алгебраических преобразований. Применение DP-метода при выводе из гипотез. Правило резолюции Робинсона .
Выводы. Задачи в логике высказываний. .
Логика предикатов .
Формулы с одноместными предикатами.
Формулы с многоместными предикатами.
Формулы с кванторами.
Законы логики предикатов с кванторами.
Дизъюнктивное расширение области действия кванторов. Конъюнктивное расширение области действия кванторов. Законы для формул со смешанными кванторами .
Нормальные формулы с предикатами.
Теории первого порядка.
Метод резолюций в логике предикатов.
Приложения логики предикатов.
Применение логики в базах данных. Применение логики к программам .
Выводы. Задачи в логике предикатов.
Логическое (сентенциальное) программирование .
Декларативная семантика программ Пролога.
Процедурная семантика программ Пролога.
Выводы.
Прикладная логика .
Схемотехника логических утверждений.
Приложения многозначной логики в моделировании схем.
Временное моделирование цифровых схем. Четырехзначное логическое моделирование .
Тестирование логических схем.
Структурное троичное тестирование цифровых схем. Структурное четырехзначное тестирование. Алгебро-топологические методы синтеза тестов логических схем .
Выводы. .
Заключение.
Вопросы к зачету.
Список литературы.
Именной указатель.