Защищенная логика
Защищенная логика — это выбора набор динамической логики , участвующий в выборе, результаты которого ограничены.
Простой пример защищенной логики таков: если X истинно, то Y, иначе Z можно выразить в динамической логике как (X?;Y)∪(~X?;Z). Это показывает осторожный логический выбор: если X выполняется, то X?;Y равно Y, ~X?;Z блокируется, а Y∪block также равно Y. Следовательно, когда X истинно, основной исполнитель действия может принимать только ветвь Y, а в случае ложности - ветвь Z. [1]
Реальным примером является идея парадокса : что-то не может быть одновременно истинным и ложным. Осторожный логический выбор — это выбор, при котором любое изменение истины влияет на все решения, принимаемые в дальнейшем. [2]
История
[ редактировать ]До использования защищенной логики для интерпретации модальной логики использовались два основных термина. Математическая логика и теория баз данных (искусственный интеллект) были логикой предикатов первого порядка. Оба термина нашли подклассы первоклассной логики и эффективно используются в разрешимых языках, которые можно использовать для исследований. Но ни один из них не мог объяснить мощные расширения с фиксированной точкой логики модального стиля.
Later Moshe Y. Vardi [3] выдвинул гипотезу, что древовидная модель будет работать для многих логик модального стиля. Защищенный фрагмент логики первого порядка был впервые представлен Хайналом Андрекой , Иштваном Немети и Йоханом ван Бентемом в их статье «Модальные языки и ограниченные фрагменты логики предикатов». Они успешно перенесли ключевые свойства логики описания , модальной и темпоральной логики в логику предикатов. Было обнаружено, что робастная разрешимость защищенной логики может быть обобщена с помощью свойства древовидной модели. Древовидная модель также может быть убедительным признаком того, что защищенная логика расширяет модальную структуру, сохраняющую основы модальной логики.
Модальные логики обычно характеризуются инвариантностью относительно бисимуляции . Также случается, что инвариантность при бисимуляции является корнем свойства древовидной модели, которое помогает определить теорию автоматов .
Типы защищенной логики
[ редактировать ]В Guarded Logic существует множество охраняемых объектов. Первый охраняемый фрагмент, представляющий собой логику первого порядка модальной логики. Защищенные фрагменты обобщают модальную количественную оценку путем обнаружения относительных закономерностей количественной оценки. Синтаксис, используемый для обозначения защищенного фрагмента, — GF . Другим объектом является логика защищенной фиксированной точки , обозначаемая как μGF, которая естественным образом расширяет защищенный фрагмент от фиксированных точек от наименьшей к наибольшей. Защищенные бисимуляции — это объекты, которые при анализе защищенной логики. Все отношения в слегка модифицированной стандартной реляционной алгебре с защищенной бисимуляцией и определимым первого порядка известны как защищенная реляционная алгебра . Это обозначается с помощью GRA .
Наряду с объектами защищенной логики первого порядка существуют объекты защищенной логики второго порядка. Она известна как защищенная логика второго порядка и обозначается GSO . Подобно логике второго порядка , защищенная логика второго порядка определяет количественно, чей диапазон над защищенными отношениями ограничивает ее семантически. Это отличается от логики второго порядка, диапазон которой ограничен произвольными отношениями. [4]
Определения защищенной логики
[ редактировать ]Пусть B — реляционная структура с универсумом B и словарем τ.
i) Множество X ⊆ B охраняется в B, если существует основной атом α(b_1,...,b_k) в B такой, что 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 ∩ Й` .
В-четвертых . Для любого f: X → Y в I и для любого охраняемого множества X` ⊆ A существует частичный изоморфный g: X` → Y` в I такой, что f и g согласуются на X ∩ X` .
Ссылки
[ редактировать ]- ^ «Формальное моделирование и анализ временной системы». Международная конференция по формальному моделированию и анализу временных систем №4 . Париж, Франция. 25–27 сентября 2006 г.
- ^ Ньювенхейс, Роберт; Андрей Воронков (2001). Логика для программирования, искусственного интеллекта и рассуждения . Спрингер. стр. 88–89 . ISBN 3-540-42957-3 .
- ^ Варди, Моше (1998). Рассуждения о прошлом с помощью двусторонних автоматов (PDF) .
- ^ «Защищенная логика: алгоритмы и бисимуляция» (PDF) . стр. 26–48 . Проверено 15 мая 2014 г.
- ^ «Защищенная логика: алгоритмы и бисимуляция» (PDF) . п. 25 . Проверено 15 мая 2014 г.