Свойство выводимости.
Логические матрицы.
Модели Крипке для логики высказываний.
Модель Крипке (англ. Kripke structure) это недерминированный конечный атомат применяемый при проверке моделeй для представления поведения системы. Модель представляется ориентированным графом вершины которого описывают достижимые состояния системы, а ребра переходы из состояния в состояние. Функция пометок сопоставляет каждой вершине множество свойств которые выполняются в соответствующем состоянии.
Формальное определение
Пусть AP
множество атомарных
высказываний.
моделью Крипке[1]
назовем четверку
состоящую
из:
конечного множества состояний
;
множества начальных состояний
;
отношения перехода
,
где
такое,
что
;
функции пометок
.
Условие накладываемое на отношение R утверждает, что каждое состояние имеет следующее. Если требуется эмулировать взаимную блокировку, в модель Крипке необходимо просто добавить ребро из состояния блокировки в себя.
Функция пометок L для каждого состояния s ∈ S определяет множество L(s) всех атомарных утверждений верных в s.
Основные понятия мЛиТа.
Теория алгоритмов, как наука, непосредственно связана с предметами математической логики и теории конечных автоматов. В Древней Греции Аристотель и его ученик Платон сформулировали основные правила логики, которые используются до нашего времени для доказательства правильности и решения логических задач.
Тео́рия алгори́тмов — наука, изучающая общие свойства и закономерности алгоритмов и разнообразные формальные модели их представления. К задачам теории алгоритмов относятся формальное доказательство алгоритмической неразрешимости задач, асимптотический анализ сложности алгоритмов, классификация алгоритмов в соответствии с классами сложности, разработка критериев сравнительной оценки качества алгоритмов и т. п.
Математическая логика – это наука о правилах формального логического мышления.
Теория автоматов изучает модели конечных автоматов, описывающие вычислительные узлы и элементы управления ЭВМ и других технических устройств.
Логические функции.
Логической ( булевой) функцией (или просто функцией) n переменных y = f(x1, x2, …, xn) называется такая функция, у которой все переменные и сама функция могут принимать только два значения: 0 и 1.
Переменные, которые могут принимать только два значения 0 и 1 называются логическими переменными (или просто переменными). Заметим, что логическая переменная х может подразумевать под числом 0 некоторое высказывание, которое ложно, и под числом 1 высказывание, которое истинно. Например, высказывание “Волга впадает в Каспийское море” является истинным и, значит, с точки зрения дискретной математики принимает значение 1, а высказывание “в неделе 8 дней” является ложным, и переменная, которая заменяет это высказывание, принимает значение 0. Имеется много высказываний, которые либо истинны, либо ложны, но о которых мы не знаем, что имеет место на самом деле. Например, высказывание “студент Петров (имеется в виду конкретный человек) имеет дома компьютер”. Такого рода высказывания требуют проверки (конечно, если нам важен этот факт). Поэтому считаем, что переменная, заменяющая это высказывание может принимать значение 0 или 1.