Защищенная логика — это набор вариантов динамической логики, участвующих в выборе, где результаты ограничены.
Простой пример защищенной логики выглядит следующим образом: если X истинно, то Y, иначе Z может быть выражено в динамической логике как (X?;Y)∪(~X?;Z). Это показывает защищенный логический выбор: если X выполняется, то X?;Y равно Y, и ~X?;Z заблокировано, и Y∪block также равно Y. Следовательно, когда X истинно, основной исполнитель действия может выбрать только ветвь Y, а когда ложно — ветвь Z. [1]
Примером из реального мира является идея парадокса : что-то не может быть одновременно и истинным, и ложным. Осторожный логический выбор — это выбор, при котором любое изменение истинности влияет на все решения, принимаемые в дальнейшем. [2]
До использования защищенной логики существовало два основных термина, используемых для интерпретации модальной логики. Математическая логика и теория баз данных (искусственный интеллект) были логикой предикатов первого порядка. Оба термина нашли подклассы логики первого класса и эффективно использовались в решаемых языках, которые можно использовать для исследований. Но ни один из них не мог объяснить мощные расширения с фиксированной точкой для логики модального стиля.
Позже Моше Й. Варди [3] высказал предположение, что древовидная модель будет работать для многих логик модального стиля. Защищенный фрагмент логики первого порядка был впервые введен Хайналом Андрекой , Иштваном Немети и Йоханом ван Бентемом в их статье «Модальные языки и ограниченные фрагменты предикатной логики». Они успешно перенесли ключевые свойства дескриптивной , модальной и темпоральной логики в предикатную логику. Было обнаружено, что надежная разрешимость защищенной логики может быть обобщена с помощью свойства древовидной модели. Древовидная модель также может быть сильным указанием на то, что защищенная логика расширяет модальную структуру, которая сохраняет основы модальных логик.
Модальные логики обычно характеризуются инвариантностью относительно бисимуляции . Также так получается, что инвариантность относительно бисимуляции является корнем свойства древовидной модели, которое помогает в определении теории автоматов .
В защищенной логике существует множество защищенных объектов. Первый из них — защищенный фрагмент, который является логикой первого порядка модальной логики. Защищенные фрагменты обобщают модальную квантификацию посредством нахождения относительных шаблонов квантификации. Синтаксис, используемый для обозначения защищенного фрагмента, — GF . Другой объект — защищенная логика с фиксированной точкой, обозначаемая μGF, естественным образом расширяет защищенный фрагмент от фиксированных точек от наименьшей к наибольшей. Защищенные бисимуляции — это объекты, которые при анализе защищенной логики. Все отношения в слегка измененной стандартной реляционной алгебре с защищенной бисимуляцией и определимостью первого порядка известны как защищенная реляционная алгебра . Это обозначается с помощью GRA .
Наряду с объектами охраняемой логики первого порядка существуют объекты охраняемой логики второго порядка. Она известна как охраняемая логика второго порядка и обозначается как GSO . Подобно логике второго порядка , охраняемая логика второго порядка квантифицирует, диапазон которой по охраняемым отношениям ограничивает ее семантически. Это отличается от логики второго порядка, диапазон которой ограничен произвольными отношениями. [4]
Пусть B — реляционная структура с универсумом B и словарем τ.
i) Множество X ⊆ B охраняется в B, если в B существует основной атом α(b_1, ..., b_k) такой, что X = {b_1, ..., b_k}.
ii) τ-структура A , в частности подструктура A ⊆ B, охраняется, если ее универсум является охраняемым множеством в A (в B ).
iii) Кортеж (b_1, ..., b_n) ∈ B^n охраняется в B , если {b_1, ..., b_n} ⊆ X для некоторого охраняемого множества X ⊆ B.
iv) Кортеж (b_1, ..., b_k) ∈ B^k является охраняемым списком в B, если его компоненты попарно различны и {b_1, ..., b_k} является охраняемым множеством. Пустой список считается охраняемым списком.
v) Отношение X ⊆ B^n охраняется, если оно состоит только из охраняемых кортежей. [5]
Защищенная бисимуляция между двумя τ-структурами A и B — это непустое множество I конечных частично изоморфных f: X → Y из A в B, такое, что выполняются условия перехода туда и обратно.
Назад: Для каждого f: X → Y в I и для каждого охраняемого множества Y` ⊆ B существует частично изоморфный g: X` → Y` в I такой, что f^-1 и g^-1 совпадают на Y ∩ Y` .
В-четвертых, для каждого f: X → Y в I и для каждого охраняемого множества X` ⊆ A существует частично изоморфный g: X` → Y` в I такой, что f и g совпадают на X ∩ X` .