有界扩展图类上的继任者不变一阶公式的模型检查
摘要：基于继承关系的一阶公式是指在结构的宇宙集上使用一个辅助继承关系的公式，而模型关系与该关系的具体解释无关。众所周知，在有限结构上，相比没有继承关系的普通一阶公式，继承关系公式更具表达能力。这自然引发了一个问题，即增加表达能力是否会增加解决模型检测问题的代价，即决定给定结构以及某个（因此也是每个）继承关系是否是给定公式的模型的问题。早先的研究已经表明，在基于维恩图的平面图类别[Engelmann等人，2012]、排除固定次小叉代数的有限结构类别[Eickmeyer等人，2013]或固定拓扑小叉代数的有限结构类别[Eickmeyer和Kawarabayashi，2016；Kreutzer等人，2016]上，将继承关系融入一阶逻辑的模型检测问题实际上不会增加额外代价。在这项工作中，我们展示出对于任何形成有界扩展类别的有限结构的基于继承关系的公式的模型检测问题是固定参数可解的。我们的结果推广了所有以前的结果，并且接近于当前已知的普通一阶逻辑在无处稠密图类别上的最佳可解性结果。
作者：Jan van den Heuvel and Stephan Kreutzer and Micha{l} Pilipczuk and Daniel A. Quiroz and Roman Rabinovich and Sebastian Siebertz
论文ID：1701.08516
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-15