守护逻辑

守护逻辑是参与选择的动态逻辑的选择集，其结果是有限的。守护逻辑的一个简单例子如下：如果X是真的，那么Y，否则Z可以用动态逻辑表示为(X?;Y)∪(~X?;Z)。这显示了一个受保护的逻辑选择：如果X成立，那么X?;Y等于Y，而~X?;Z受阻，Y∪阻也等于Y。

因此，当X为真时，行动的主要执行者只能采取Y分支，而当假时则采取Z分支。一个现实世界的例子是悖论的概念：一件事不能既是真的又是假的。

一个受保护的逻辑选择是指，真的任何变化都会影响到下一步的所有决定。

在使用守恒逻辑之前，有两个主要术语用于解释模态逻辑。数学逻辑和数据库理论（人工智能）是一阶谓词逻辑。

这两个术语都找到了第 一类逻辑的子类，并有效地用于可解语言，可用于研究。但都无法解释强大的定点扩展到模态风格的逻辑。后来，MosheY.Vardi提出了一个猜想，即树状模型对许多模态风格的逻辑都有效。

一阶逻辑的受保护片段是由HajnalAndréka,IstvánNémeti和JohanvanBenthem在他们的文章《模态语言和谓词逻辑的受约束片段》中首次提出的。他们成功地将描述、模态和时间逻辑的关键属性转移到了谓词逻辑。

他们发现，守恒逻辑的稳健可解码性可以用树模型属性来概括。树模型也可以有力地表明，守恒逻辑扩展了模态框架，保留了模态逻辑的基本要素。

模态逻辑的特点一般是在二重化下的不变量。碰巧的是，双映射下的不变性是树模型属性的根源，它有助于定义自动机理论。

在守护逻辑中，存在许多守护对象。第 一个是守护片段，它是模态逻辑的一阶逻辑。

守护片段通过寻找量化的相对模式来概括模态量化。用来表示守护片段的语法是GF。另一个对象是被守护的定点逻辑，表示为μGF，自然地将被守护的片段从最小的定点扩展到最 大。守护的双映射是分析守护逻辑时的对象。在一个稍加修改的标准关系代数中，所有的关系都具有守卫的双映射和一阶可定义，被称为守卫的关系代数。这是用GRA表示的。与一阶守恒逻辑对象一起，还有二阶守恒逻辑的对象。它被称为守卫的二阶逻辑，用GSO表示。

与二阶逻辑类似，有守卫的二阶逻辑的量化，其范围在有守卫的关系上限制了它的语义。这与二阶逻辑不同，二阶逻辑的范围被限制在任意关系上。

让B是一个具有宇宙B和词汇表τ的关系结构。i)如果在B中存在一个基础原子α(b_1,...,b_k)，使得X={b_1,...,b_k}，则一个X⊆B的集合在B中是受保护的。ii）一个τ结构A，特别是一个子结构A⊆B，如果它的宇宙是A（在B）中的一个受保护的集合，那么它就是受保护的。iii)一个元组（b_1,...,b_n）∈Bn，如果{b_1,...,b_n}⊆X，对于一些受保护的集合X⊆B，则在B中是受保护的。iv)如果一个元组（b_1,...,b_k）∈Bk的成分是成对的，并且{b_1,...,b_k}是一个被看守的集合，则该元组在B中是一个被看守的列表。

空列表被认为是一个受保护的列表。v)如果一个关系X⊆Bn只由受保护的图元组成，那么它就是受保护的。

两个τ结构A和B之间的守护双映射是一个非空的集合I，该集合由A到B的有限部分同构f:X→Y组成，从而满足前后条件。背面。对于I中的每一个f:X→Y，以及对于每一个守卫集Y`⊆B，在I中存在一个部分同构的g:X`→Y`，使得f-1和g-1在Y∩Y`上一致。第四对于I中的每一个f:X→Y，以及对于每一个受保护的集合X`⊆A，在I中存在一个部分同构的g:X`→Y`，使得f和g在X∩X`上一致。