Irina Shoshmina

Программная реализация конечных автоматов

Структура Крипке

CTL - логика ветвящегося времени

CTL. Базовые операторы

Семантика формул LTL

Выражение свойств систем в LTL

Время: линейное или ветвящееся?

Линейная темпоральная логика. Синтаксис

ВременнАя логика

Модальности

Требования, зависящие от времени

Семантика CTL формул

Идея алгоритма проверки модели для CTL

Проверка модели CTL-формул

Базисы CTL

Алгоритм маркировки состояний подформулами CTL II

Алгоритм маркировки состояний подформулами CTL I

Пример проверки выполнимости формулы CTL

Проверка корректности системы управления микроволновой печью

Резюме по методу проверки модели для CTL

Представление структуры Крипке с помощью BDD

Символьные алгоритмы проверки выполнимости темпоральных формул

Идея компиляции структуры Крипке по программе

BDD vs взрыв числа состояний при верификации

Примеры верификации программ в Политехе

Пример индустриального использования метода проверки модели

Общая характеристика достижений метода проверки модели

Слабейшее предусловие программы

Аксиоматический метод верификации программ А. Хоара

Замечание о программировании по контракту

О сложности дедуктивной верификации

Инварианты циклов в задачах о вагонах и хамелеонах

Инварианты в вычислительных программах

Задача о кофейных зернах и игры со спичками

Инварианты цикла

Разработка программ корректных по построению

Метод Флойда и тестирование

Задача о голландском флаге

Реагирующие системы

Интерливинг в параллельных программах

Параллелизм - источник сложности анализа реагирующих систем

Программа как система переходов

Абстрагирование при моделировании реагирующих систем

Проблема взаимно исключающего доступа

О проблеме корректности программных систем управления

Несет ли программист ответственность за человеческие жизни?

Финансовые потери от программных ошибок

Метод проверки модели

Трудность доказательства корректности реагирующих систем

Примеры аксиоматических теорий

Основные компоненты аксиоматической теории

Необходимость формализации математических доказательств

Аксиоматическая теория Гильберта исчисления высказываний

Условные выполнимость и выводимость

Свойства аксиоматических теорий

Свойства аксиоматической теории Гильберта исчисления высказываний

Постановка задачи верификации программ

Верикация - метод обеспечения качества программ

Разница между тестированием и верификацией

Слабейшее предусловие для оператора присваивания

Частичная и тотальная корректность программы

Проблема построения слабейшего предусловия

Индуктивный метод Флойда

Сильнейшее постусловие программы

Доказательство корректности ациклических программ

Слабейшее предусловие для оператора выбора

Предваренная нормальная форма

Особенности метода резолюции в логике предикатов

Категорические силлогизмы Аристотеля

"Правильные" и "неправильные" умозаключения в логике предикатов

Сколемовская форма формул логики предикатов

Примеры с методом резолюций в логике предикатов

Унификация атомарных предикатов

Постановка задачи логического вывода в логике предикатов

Силлогизм Barbara и бурундукотигр

Пациенты и знахари

Парадокс Эпименида

Пара задач с математическими объектами

Структура программы на ПРОЛОГе

Мир вампуса и метод резолюции в логике предикатов

Запрос к базе данных и метод резолюции

Несколько программ на ПРОЛОГе

Программа определения родства на ПРОЛОГе

Формализация информации с помощью логики предикатов

Синтаксис логики предикатов

Ограниченность логики высказываний при формализации объектов реального мира

Разбор структуры предикатной формулы

Использование логики предикатов в примерах

Семантика логики предикатов

Определение эквивалентности (равносильности) формул логики предикатов

Примеры эквивалентных преобразований формул логики предикатов

Общезначимые и невыполнимые формулы в логике предикатов

Примеры известных равносильных и неравносильных формул логики предикатов

Определение ограниченных кванторов

Эквивалентные преобразования с ограниченными кванторами

Примеры формализации с использованием ограниченных кванторов

Математические определения и ограниченные кванторы

Мир вампуса и ограниченные кванторы

Закон о продаже оружия и ограниченные кванторы

Кванторы и область их действия

Примеры проверки "правильности" схем умозаключений

Методы решения задачи SAT

Частные случаи задачи SAT

Проблема адекватности формализации на примере задачи Кислера

Когда логический вывод "не работает"?

Проверка "правильности" схемы умозаключения по таблице истинности

Силлогизмы и "новое знание"

Основная теорема логического вывода

Задача Порецкого о птицах - пример задачи с 4-мя переменными

Тривиальные и неправильные схемы умозаключений

Проверка "правильности" схемы умозаключения через КНФ или ДНФ

Формулировка основной теоремы логического вывода через невыполнимую формулу

Метод резолюции в логике высказываний. Основные понятия

Использование метода резолюций в логике высказываний

Непротиворечивость и полнота метода резолюций в логике высказываний

Силлогизмы и метод резолюций в логике высказываний

Интерпретация резолютивного вывода в логике высказываний на естественном языке

Хорновские дизъюнкты в примере из химии

Формулировка проблемы выполнимости SAT

Практические задачи как задачи SAT

SAT CNF

Алгоритм DPLL

Преобразование высказываний естественного языка в формулы

Задачи с "неочевидными" фактами

Абстрагирование в логике высказываний

Семантика формул логики высказываний

Синтаксис формул логики высказываний

Схема решения задач в математической логике

Типы логических формул

Проверка высказываний на общезначимость

Эквивалентные преобразования высказываний

Упрощение сложных высказываний

Что такое структура математического доказательства

Задача про стражников

Использование эквивалентных формулировок теорем в доказательствах

Структура теорем о необходимости и достаточности

Конъюнкция утверждений как способ упростить структуру доказательства

Максимально сильное логическое следствие

Принцесса, тигр и инспектор Крейг

Формализация задачи о роботе-сапере

Алгоритм действий робота-сапера

Экспоненциальный рост представлений двоичных функций

BDD - эффективный способ представления двоичных функций

Бинарные операции над BDD

Конечный автомат как преобразователь с памятью

Примеры конечных автоматов

Аппаратная реализация конечных автоматов

Формальное определение конечных автоматов

Автомат по продаже кофе и программа выбрасывания пробелов

"Однорукий бандит"

Системы управления микроволновой печкой, часами и микрокалькулятором

Интеллектуальная лампа и мобильный телефон

Клеточные автоматы и новая наука С. Вольфрама

Клеточные автоматы как конечные автоматы

Протокол выбора лидера

Протокол двухфазного соглашения

Применение клеточных автоматов

Релейно-контактные схемы и двоичные функции

"Прямое" применение BDD

BDD и аппаратные схемы

"Непрямое" применение BDD

Символьное представление множеств и операции над ними

Операции над характеристическими функциями отношений

Построение цифровой аппаратуры с помощью двоичных функций

Система управления входом в метро

Пример с отношением на множестве

Символьное представление конечных функций

Символьный алгоритм решения проблемы достижимости

Замкнутые классы двоичных функций. Примеры базисов

Формулировка теоремы Поста. Доказательство необходимого условия

Замкнутые классы двоичных функций Э. Поста

Суперпозиция двоичных функций. Идеи Э.Поста

Задачи, связанные с понятием функционально полных множеств

Доказательство достаточного условия теоремы Поста. Шаг 1 - построение констант

Докзательство достаточного условия теоремы Поста. Шаги 2 и 3 - построение отрицания и конъюнкции

Примеры применения теоремы Поста

Как построить базис с помощью теоремы Поста

Функционально полные множества. Базисы

Двоичные функции как механизм абстракции

Управляемые вентили разные реализации

Электромеханические реле как реализация двоичных функций

Карты Карно для 5-ти, 6-ти двоичных переменных

Карты Карно. Минимизация КНФ. Код Грея.

Примеры минимизации двоичных функций для электронных часов и варочной плиты

Карты Карно от 4-х переменных

Карты Карно

Необходимость минимизации двоичных функций

Переход от одной нормальной формы двоичных функций к другой

Суммаризация нормальных форм двоичных функций. Полином Жегалкина

Конъюнктивная нормальная форма двоичных функций

Дизъюнктивная нормальная форма

Значение основной теоремы теории двоичных функций

Лемма Шеннона и доказательство основной теоремы теории двоичных функций

Свойства двоичных функций

Формулировка основной теоремы теории двоичных функций

Переход между разными формами представления двоичных функций

Семантическое дерево двоичной функции

Двоичные функции от n переменных. Формулы

Таблицы истинности. Двоичные функции от 1-ой, 2-х, 3-х переменных

Построение схемы отображения электронных часов

Двоичные функции как конечные функциональные преобразователи

Логика и верификация программ

Логика и интеллект (искусственный и не только)

Формулировки занимательных задач

Логическая эквивалентность, логическое следствие, логический вывод

Динамические структуры и двоичные функции

Проблема вычисления значения двоичной функции

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

Структура курса "Математическая логика"