混合逻辑（二）

此外，通过省略两种粘合剂↓和∀获得的较弱的混合逻辑已成为广泛勘探的主题。 事实证明，这种无粘合剂的逻辑和许多变体是可判定的。 在纸张，布莱克本和马克思（1999）中，在各种帧中的混合模态和时态逻辑给出了许多复杂性结果，例如任意，传递，线性和分支。 值得注意的是，在任意帧上，在PSPACE中可解除粘合剂的混合逻辑的可靠性问题，与普通模态逻辑的决定可靠性的复杂性相同。 因此，杂交普通模态逻辑提供了更有表现力的力量，但复杂性保持不变。 在模拟莫代尔逻辑内的标称值时已经进行了一些工作，参见Kracht和Wolter（1997）。

任何普通的模态配方在帧上表达了一个Monadic二阶属性，并且众所周知，对于一些模态公式，包括所谓的Sahlqvist公式，二阶属性等同于一阶属性。 在纸质戈兰科和Vakarelov（2006）中，这也被认为是一类杂化逻辑公式，包括标称逻辑公式。 存在用于计算普通模态公式的一阶等同物的几种算法。 一种这样的算法，SQEMA，在纸张Conradie，Goranko和Vakarelov（2006）中，延伸到包括在Goranko和Vakarelov（2006）中考虑的混合逻辑公式。

如上所述，先前引入了混合时态逻辑，以处理时间哲学中的特定问题，但在先前（1968年）中，第十四章（在新版中的第XIV章（2003年）），他还表明杂交时态逻辑可以取代由HANS KAMP引入的二维时间逻辑在1967年在1967年循环中迁移的未发表的材料，后来包括在Kamp（1971）中。 维度只是相对于评估公式的瞬间数量，因此添加混合逻辑机械使得两个维度能够被一个替换。 这项工作最近被Blackburn和Jørgensen的一些论文随访了，参见Blackburn和Jørgensen（2016A）概述。 我们现在介绍了这一工作行的简要剪影，适应了目前入境的术语。 有问题的混合逻辑的版本现在具有指定的标称，每个型号都有一个指定时间t0，使得I）相对于T0和II评估的任何独立公式），标称现在是指T0。 更正式地，我们采用（M，T0），g⊨φ表示m，g，t0νφ的惯例，我们只考虑分配g其中g（现在）= t0。 请注意，现在，标称值被视为独立公式，在本语法中有效，但这不是任何其他标称的情况。 这种新的有效概念是Blackburn和Jørgensen称为上下文有效性。 纸张Blackburn和Jørgensen（2013）给出了一个完整的WRT的Axiom系统。 这种语境有效性的概念。 这篇论文的纸张Blackburn和Jørgensen（2012）给出了完整的Tableau系统，但本文的语义符合Kamp的原始二维语义。 两篇论文也考虑进一步的股票，如昨天，今天和明天。

纸黑牌和jørgensen（2016b）采用混合时态逻辑将汉斯·雷诺纳巴赫的想法与如何代表自然语言时期。 优先于上面描述的众所周知的时态算子，而Reichenbach优选的时间参考，即特定时间，Reichenbach（1947）。 事实证明，这两种方法可以组合，这不是先前自己所采取的路线 - 请参阅Blackburn和Jørgensen（2016B）中给出的帐户，

混合逻辑概念已应用于许多不同的地方，例如，纸张Areces和Fervari（2021）将混合算子添加到XPath，这是一个广泛使用的XML的查询语言，用于描述数字文本的标记语言。 混合逻辑也被用于为规范逻辑添加表现力的功率，以捕获计算系统的某些属性，参见Neves，Madeira，Martins，Barbosa（2016）。 此外，应该提到类似于混合逻辑的逻辑在描述逻辑区域内发挥着核心作用，它是用于人工智能中的知识表示的逻辑系列，参见纸张Blackburn和Tzakova（1998）和Carlos Areces'博士论文（2000）。

6.混合逻辑的公理

许多论文处理了混合逻辑的公理，例如Gargov和Goranko（1993），Blackburn（1993）和Blackburn和Tzakova（1999）。 在纸质GARGOV和GORANKO（1993）中，给出了一种用于混合逻辑的公理系统，并显示出系统与一组附加公理延伸，这是纯公式的（即所有命题符号是标称的公式），然后，相对于验证所讨论的公理的帧，延伸的Axiom系统是完整的。 纯粹的公式对应于可访问性关系的一阶条件（CF.上面的翻译STA），因此可以简单地以均匀的方式获得具有一流条件的新混合逻辑的AXIOM系统，只需均匀地获得适当的公理。 因此，例如，如果将公式C→◻¬c-C添加为公理，则所得系统相对于不确定的框架完成，如前所述。 参见纸张Blackburn第4节（2000）的规则讨论。

Gargov和Goranko（1993）的证明系统利用复杂的规则（称为COV），其中包含规则的活动部分的公式模式可以是任意的; 实际上，活动部分嵌入了模态运算符的任意深嵌套。 Blackburn和Tzakova（1999）表明，使用称为粘贴的更简单规则，可以使用满足操作员以更简单的规则制定一个更标准的格式，使得系统仍然仍然完成纯轴。

纸质黑招和十个Cate（2006）调查了正统证明规则，它是没有副条件的证明规则，结果表明，如果需要使用纯公式延长完整性，则在Axiom系统中是不可缺少的非正统校正规则无粘合剂的混合逻辑。 然而，在包括↓粘合剂的更强的混合逻辑的情况下，可以给出仅涉及正统证明规则的公理系统。 另请参阅BRAÜNER（2011A）用于混合逻辑的另一个AXIOM系统以及用于直觉混合逻辑的公理系统，以及纳尔逊的滞后逻辑N4的杂交（与哥斯达和马丁斯相比（2017年）考虑另一个滞后的混合逻辑）。 对直觉混合逻辑的调查可以在Braüner（2011B）中找到。

7.混合逻辑的分析方法

与普通的模态逻辑相比，混合逻辑的Tableau 通常，当给出模态地图，绅士或自然扣除系统时，它是一个特定的模态逻辑，并且已经出现了以统一的方式在不引入金属语言机制的情况下为模态逻辑制定这种系统的问题。 这可以通过杂交来补救，即模态逻辑的杂交使得能够为广泛的逻辑制定均匀的Tableau，Gentzen和自然扣除系统。 纸张布莱克本（2000）介绍了一个具有这种理想的混合逻辑的Tableau系统：类似于Blackburn和Tzakova的Axiom系统（1999），如果Tableau系统延长了一套纯粹的制度系统，则保持完整性公理，即，在Tableau建筑期间允许将一组纯公式添加到Tableau中。 Blackburn（2000）的Tableau系统是在Bolander和Braüner（2006）中给出的混合逻辑的无合体逻辑的无活粘片段的决定程序的基础。 这篇作品中的论文博士兰和布莱克本（2007年）和Bolander和Blackburn（2009年）一直在继续。 论文Cerrito和Cialdea（2010）呈现出混合逻辑的另一个基于Tableau的决定程序。 混合逻辑的其他决定程序，也基于校验理论，给出了纸张Kaminski和Smolka（2009）。 后者纸张的程序基于涉及简单类型的λ微积分的混合逻辑的高阶制定。

汉森，博瓦尔德和Braüner（2018年）给出了一种基于Tableau的决定程序，即多价值的混合逻辑，即混合逻辑，其中双价古典逻辑基础一直以多价位的逻辑基础推广涉及具有有限居民代数的结构的真实值空间。 Hansen（2010）为动态认知逻辑的动态认知逻辑的杂交版本提供了基于Tableau的决定程序，称为公共止回逻辑。 这也是汉森博士（2011）的主要问题。

Brailner（2011A）书中探讨了杂交逻辑的自然扣除风格证明理论。 本书还为混合逻辑提供了无紫外线搜索系统。 通过标准化的自然扣除系统证明了切Freeness，但也可以直接证明这样的结果，请参阅Indrzejczak（2016）。 Braüner（2011A）的自然扣除和绅士系统可以通过对应于所谓的几何理论表达的可访问性关系的一阶条件（这相当于将Tableau和Axiom系统与纯公理的延伸）相对应延长。 另见Braüner和de Paiva（2006），其中一种自然扣除系统，用于直觉混合逻辑（Braüner（2011A）的第8章）。

20世纪90年代，探索了类似于混合逻辑的逻辑和自然扣除系统，由Jerry Seligman探讨了20世纪90年代，请参阅Seligman（2001）的概述。 特别是，Seligman开发了与任意公式合作的证明系统，而不仅仅是满意语句，后者对于混合逻辑的大多数证明系统而言，令人满意的运算符用于访问模型隐藏的信息。 在Seligman（1997）中引入了这种风格的自然扣除系统，该系统在Brain（2011A）书籍第4章中进一步发展。 塞利格曼证明风格的Tableau系统已被考虑在Blackburn，Bolander，Braüner和Jørgensen（2017）中，其中提供了句法完整性证据。 在Jørgensen，Blackburn，Bolander，Braüner（2016）中给出了Tableau系统的语义完成。 在这些系统中的推理不直接依赖于全局编码，即满足操作员可以实现这些系统，因此可以更加符合标准Kripke语义的模态逻辑的本地字符。 事实上，这种更多的本地推理风格使这些系统适用于在某些心理推理任务中进行正式化的透视推理，参见Braüner（2014b）以及Braüner，布莱克本和多尚纳斯（2016）。

如上所述，Papers Blackburn，Bolander，Braüner和jørgensen（2017）和jørgensen，Blackburn，Blackander，Braüner（2016）为Seligman-Squiny Systems提供了证明用于混合逻辑。 基于这些结果，这些系统的完整性来自（2021）和来自Blackburn和Villadsen（2020）的使用验证助理Isabelle / Hol完全正式。

解决了解决方案和模型检查的一些工作，参见ARECES，DE RIJKE和DE NIVELLE（2001）以及ASECES和GORIN（2011年），以及作为FRANCESHET和DE RIJKE（2006）以及作为模型检查结果的Lange（2009）。

8.量化的混合逻辑

我们分别对数量的混合逻辑进行治疗。 一阶模态逻辑来自许多不同的版本，这也是一阶混合逻辑的情况。 首级混合逻辑的Tableau系统可以在纸黑招和马克思（2002）中找到。 用于一阶混合逻辑的自然扣除和公理系统可以在Braüner（2011A）的第6章中找到，本书第7章对海拔一阶混合逻辑的自然扣除。 本文Indrzejczak（2020）给出了具有Lambda运算符的一阶混合逻辑的先生样式序列演算，以及存在和义识别。 纸芭芭巴，马丁斯和Carreteiro（2014）给出了一阶混合逻辑的片段，称为公式一阶混合逻辑。

非常卓越的是，一阶混合逻辑提供了证明插值定理所需的功能：虽然在多个着名的一阶模态逻辑中插值失败，但其杂交的对应物具有此属性，请参阅Areces，布莱克本和马克思（2003年）以及布莱克本和马克思（2003）。 第一篇论文提供了一个模型 - 理论的插值证明，而第二纸张给出了一种基于Tableau系统计算内立板的算法。

纸张，Blackburn，Huertas和Manzano（2014）涉及高阶模态逻辑的混合逻辑版本（即建立在教堂简单的类型理论上的模态逻辑）。 给出了Axiom系统，并证明了WRT的完整性。 Henkin型语义。 Blackburn，Huertas，Manzano和Jørgensen（2014）延长了这些结果，以包括令人沮丧的粘合剂，并从一阶逻辑的有界碎片中翻译，并从一阶逻辑的界定（见上文）。

而不是将标称值作为第二种命题符号引入，而是使用命题量子与Q运算符一起使用，定义如下：

qp =◊p∧∀q（◻（p→q）∨◻（p→¬q））

这里的◻和◊是普遍方式的盒子和钻石形式。 将普通命题符号P以Q运算符为前缀的结果将p转换为标称值。 要更加精确，请将命题量词∀q∀qq范围放在所有世界上，qp表示p表示单例设置，即，p是标准标称。 但是，另一种方法可以解释命题量词，称为一般（或Henkin）方法，其中命题量词范围在预选的世界亚群上。 解释了这两种不同的方式，Q运营商产生了两个不同的名义“物种”，事实证明，这两个物种就普遍实例化规则而行为不同。 这是在纸黑招，Braüner和Kofod（2020）中的调查，它为具有Henkin式命题量词的混合逻辑的Tableau系统，其中包含了两个名义。 此外，该论文描述了这种形式定义的“物种分裂”的方式对应于可以在先前的作品中检测到的标称值的两个直觉。

自20世纪90年代中期以来，杂交逻辑的工作蓬勃发展。 我们将读者推荐给参考书目中的出版物以获取进一步的参考。 此外，请参阅下面的Internet资源。