Tractability frontiers in probabilistic team semantics and existential second-order logic over the reals
概率团队语义是概率依赖的逻辑分析框架。我们的重点是概率包含逻辑及其扩展的公理化，复杂性和表达性。我们确定了一个自然片段的存在性二阶逻辑与添加剂真正的算术，准确地捕捉概率包含逻辑的表达能力。此外，我们将这些形式主义的线性规划，这样做得到PTIME数据复杂度的逻辑。此外，在有限结构上，我们证明了具有加性实算术的完全存在二阶逻辑只能表示NP性质。最后，我们在原子层次上给出了概率包含逻辑的一个合理而完整的公理化。
2021-12-21 cs.LO
Counting of Teams in First-Order Team Logics
本文研究了从#P到# $\cdot$ NP范围内的计数复杂性类的描述复杂性。Fagin用存在二阶逻辑刻画NP的一个推论是，#P可以逻辑上描述为一阶公式中计算满足对自由关系变量的赋值的函数类。在本文中，我们将这项研究扩展到类以外的#P和扩展的一阶逻辑与团队语义。这些团队为基础的逻辑是密切相关的存在的二阶逻辑和它的片段，因此我们的结果也揭示了复杂的计数扩展的FO塔斯基的语义。我们的结果表明，类# $\cdot$ NP可以用独立逻辑和存在二阶逻辑进行逻辑刻画，而依赖逻辑和包含逻辑分别产生了类# $\cdot$ NP和类#P的子类.我们的主要技术结果表明，单调布尔$Σ_1$公式满足赋值的计数问题是# $\cdot$ NP-完全的，对于依赖逻辑生成的函数类也是完全的.
2020-12-29 cs.CC cs.LO
Complex Markov Logic Networks: Expressivity and Liftability
FEE CTU in Prague（布拉格捷克理工大学电气工程学院）
研究了马尔可夫逻辑网络的表达性。我们介绍复杂的MLN，它使用复值的权重，我们表明，与标准MLN与实值权重，复杂的MLN是充分表达。然后，我们观察到，离散傅立叶变换可以计算使用加权一阶模型计数（WFOMC）与复杂的权重，并使用此观察设计一个算法计算关系的边缘多面体，需要大大减少调用WFOMC预言比最近的算法。
2020-07-16 cs.AI cs.LG cs.LO
Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
我们证明了分支时间时序逻辑CTL和CTL*，以及交替时间时序逻辑ATL和ATL*，在具有单个命题变量的语言中与在完整语言中一样具有语义表达性，即，有无限的命题变量由此可见，对于CTL和ATL，用单个变量的可满足性是EXPTIME-完全的，而对于CTL* 和ATL*，用单个变量的可满足性是2 EXPTIME-完全的，即，对于这些逻辑，只有一个变量的公式的可满足性与任意公式的可满足性一样困难。
2019-01-18 cs.LO
Expressivity within second-order transitive-closure logic
二阶传递闭包逻辑SO（TC）是一种表达性声明语言，它捕获了复杂性类PSPACE。它的一元片段MSO（TC）已经允许以自然和优雅的方式表达各种NP困难甚至PSPACE困难的问题。由于SO（TC）提供了一个有吸引力的框架，用于在声明式指定的计算方面表达属性，因此理解语言的不同特征的表达性是很有趣的。本文重点讨论片段MSO（TC），以及纯存在片段SO（2 TC）（E）;在2 TC中，TC算子仅绑定关系变量的元组。我们建立，关于表达能力，SO（2 TC）（E）崩溃到存在一阶逻辑。此外，我们还研究了MSO（TC）与具有计数特征的MSO（TC）的扩展（CMSO（TC））以及与阶不变MSO的关系。我们发现CMSO（TC）和MSO（TC）的表达能力是一致的。此外，我们建立，在一元词汇表，MSO（TC）严格包含顺序不变的MSO。
2018-04-16 cs.LO
Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals
University of Helsinki（赫尔辛基大学）；University of Sheffield（谢菲尔德大学）
本文在因果多团队语义下，通过线性不等式族和闭包条件，完全刻画了表达概率语句、条件化和干预反事实的几种逻辑的表达性，并揭示了严格张量析取在捕获所有线性不等式中的必要性。
2026-06-23 cs.LO math.LO
Complexity and expressivity of propositional dynamic logics with finitely many variables
研究了命题动态逻辑有限变量片段可满足性的复杂性。我们认为三种形式主义属于三个代表性的复杂性类，广泛理解，-经常PDL，这是EXPTIME-完整的，PDL的交集，这是2 EXPTIME-完整的，PDL与并行组合，这是不可判定的。我们表明，对于这些逻辑中的每一个，即使我们只允许仅由命题常量（即没有命题变量）构建的公式作为输入，可满足性的复杂性也保持不变。此外，我们表明，这是一个后果的丰富的表达能力的变量免费片段：对于所有的逻辑，我们认为，这样的片段是整个逻辑的语义表达。我们推测，这是PDL风格的代表，以及密切相关的逻辑。
2019-01-18 cs.LO math.LO
Towards a Model Theory of Ordered Logics: Expressivity and Interpolation (Extended version)
我们考虑家庭的保护和无保护有序逻辑，构成一个最近重新发现的家庭的可判定的片段的一阶逻辑（FO），其中的顺序量化的变量一致的顺序，这些变量出现作为参数的谓词。虽然他们的可满足性问题的复杂性现在已经很好地建立起来，但是他们的模型理论却知之甚少。本文的目的是提供一些见解。我们首先提供了合适的概念，有序逻辑的互模拟。接下来，我们采用互模拟来比较有序逻辑的相对表达能力，并将我们的逻辑描述为FO a la van Bentham的互模拟不变片段。然后研究了Craig插值性质~（CIP）。我们驳斥了另一个说法，从臭名昭著的工作珀迪，通过显示，长笛和向前的碎片不享受CIP。我们补充这一结果表明，有序片段和保护有序逻辑享有CIP。这些积极的结果依赖于新的和相当复杂的模型结构，充分利用了我们的逻辑的“forwardness”。
2022-06-23 cs.LO
A Note on Higher Order and Variable Order Logic over Finite Models
我们证明了描述复杂性的结果在高阶逻辑中的扩展，以捕获图灵机的表达能力，它具有有限的交替次数，其时间或空间是由有限的指数塔。因此，我们有一个基本的逻辑特征。我们还考虑了一些不动点算子和一元高阶逻辑的表达性。最后，我们证明了有限结构上的变序逻辑包含了分析层次。
2014-07-15 cs.LO
Expressivity of Planning with Horn Description Logic Ontologies (Technical Report)
Saarland University（萨尔大学）；University of Freiburg（弗莱堡大学）
人工智能规划中的状态约束在全球范围内限制了法律环境状态。标准规划语言做出封闭域和封闭世界的假设。在这里，我们解决开放世界的状态约束正式规划的描述逻辑（DL）本体。以前，这种DL和规划的结合已经被研究用于轻型DL DL-Lite。在这里，我们提出了一种新的编译方案，标准PDDL派生谓词，这适用于更有表现力的DL和基于DL查询到数据库的可重写性与分层否定。我们还提供了一个新的可重写性结果的DL霍恩ALCHOIQ，这使我们能够将我们的编译方案相当表达的本体。相比之下，我们表明，在轻微的扩展角SROIQ没有这样的编译是可能的，除非弱指数层次崩溃。最后，我们表明，我们的方法可以优于以前的工作，现有的基准规划与DL本体，是可行的新基准利用更具表现力的本体。这是AAAI 22接受的论文的扩展版本。
2022-03-17 cs.AI cs.CC cs.LO
Comparing the Update Expressivity of Communication Patterns and Action Models
本文证明动态认知逻辑中行动模型逻辑与通信模式逻辑在更新表达力上不可比较，并进一步表明在基于历史语义且限制于静态解释系统时，行动模型逻辑的更新表达力严格强于通信模式逻辑。
2023-07-11 cs.DC cs.LO
Complexity of Propositional Logics in Team Semantics
我们分类的可满足性，有效性和模型检测问题的命题独立性，包含性和团队逻辑的计算复杂性。我们的主要结果表明，命题组逻辑的可满足性和有效性问题是完全的交替指数时间与多项式多交替。
2017-01-05 cs.CC cs.LO math.LO
Axiomatizations of Team Logics
在一个模块化的方法，我们提升希尔伯特式证明系统的命题，模态和一阶逻辑广义系统为各自的团队为基础的扩展。我们对Väänänen的一阶群逻辑TL的无依赖片段FO（~），命题群逻辑PTL，量化命题群逻辑QPTL，模态群逻辑MTL，以及相应的依赖、独立、包含和排除逻辑，得到了合理而完整的公理化.作为完备性证明的关键步骤，我们证明了上述逻辑在某种意义上承认从公式中消除模态和量词的语义保持性。
2018-03-26 cs.LO
Decidability of predicate logics with team semantics
我们研究了基于团队语义的谓词逻辑的复杂性。证明了二元独立逻辑和二元包含逻辑的可满足性问题都是NEXPTIME-完全的。此外，我们表明，两个变量的依赖逻辑的有效性问题是不可判定的，从而解决了一个开放的问题，从团队语义文献。我们还简要地分析了依赖逻辑的Bernays-Schönfinkel-Ramsey前缀类的复杂性。
2016-06-18 cs.CC cs.LO math.LO
Logics for Epistemic Actions: Completeness, Decidability, Expressivity
我们考虑动态版本的认知逻辑，如Baltag和Moss的“认知程序的逻辑”（2004）中所阐述的。这篇论文提出了一种动态认知逻辑的逻辑语言（实际上是由动作签名参数化的语言家族）。已有研究表明，该语言的有效性是Pi-1-1-完备的，因此不存在递归公理化的完备逻辑系统，而本文则证明了无动作迭代的片段的弱完备性结果，以及无动作迭代的片段和常识的强完备性结果。我们的工作涉及到术语重写理论的迂回。该论点使用模态过滤，因此我们得到有限的模型属性，因此可判定性。我们也给我们最大的语言翻译成PDL，从而获得第二个证明的可判定性。本文最后给出了一些关于表达能力的结果。这些主要涉及比较动作迭代自由语言与模态逻辑增强传递闭包运算符。我们回答了一个自然的问题，我们通过不同的动作签名获得的语言：我们证明了一个逻辑语言与运营商的私人公告更有表现力比一个公共公告。
2022-03-13 cs.LO math.LO
Parameterized Complexity of Weighted Team Definability
在这篇文章中，我们研究的复杂性加权团队可定义的逻辑与团队语义。这个问题是一个自然的模拟研究最多的问题之一，参数化的复杂性，加权Fagin定义的概念，这是制定在满足一阶公式与自由关系变量。我们专注于加权团队可定义性的参数化复杂性为一个固定的公式φ的中心团队为基础的逻辑。给定一个一阶结构A和参数值k作为输入，问题是确定A，T是否为某个规模为k的团队T建模phi。我们展示了几个结果，这个问题的依赖，独立和包含逻辑公式的复杂性。此外，我们还与加权团队定义的复杂性，在著名的W-层次结构以及paraNP的复杂性类。
2023-02-01 cs.CC cs.LO
Temporal Team Semantics Revisited
本文提出基于时间评估函数的时间团队语义学，用于规范异步超属性，并证明同步TeamLTL的嵌入、某些TeamCTL片段MC的高度不可判定性，以及TeamCTL*到交替异步Büchi自动机的翻译及可判定性结果。
2024-02-05 cs.CC cs.LO
Synchronous Team Semantics for Temporal Logics
University of Tübingen（蒂宾根大学）；Institut für Theoretische Informatik, Leibniz Universität Hannover（汉诺威莱布尼茨大学理论计算机科学研究所）；School of Computing Science, University of Glasgow（格拉斯哥大学计算科学学院）；Department of Computer Science, Aalborg University（奥尔堡大学计算机系）
本文为LTL和CTL提出团队语义，使其能表达超性质，研究其计算复杂度并证明带有团队语义的LTL是HyperLTL的可行替代方案。
2026-10-06 cs.LO
The flattening operator in team-based logics
本文系统研究团队语义中的扁平化算子，分析其为依赖、匿名、包含和排除等团队逻辑增添的表达能力。
2025-05-27 cs.LO
The Transformation Logics
University of Oxford（牛津大学）
本文提出一族以变换算子为核心的新型时序逻辑，尤其利用基于半群的算子构建表达能力与复杂度递增的层级，为不同应用的权衡需求提供新框架。
2024-09-06 cs.AI cs.FL cs.LO
Enumeration Complexity of Poor Man's Propositional Dependence Logic
依赖逻辑（英语：Dependence logics）是一个现代的独立和依赖逻辑家族，模仿数据库理论的概念。本文旨在开创依赖逻辑领域中枚举复杂性的研究，从而对数据库查询答案的枚举问题提出一个新的观点。因此，作为第一步，我们调查的问题，枚举所有满足队的公式从一个给定的片段命题依赖逻辑。我们区分由任意函数限制团队规模和参数化版本，其中参数是团队规模。我们表明，多项式延迟可以达到多项式，否则在参数化设置，我们达到FPT延迟。然而，构造的具有多项式延迟的枚举算法需要指数空间。我们证明了一个增量多项式延迟算法存在，它只使用多项式空间。相反，我们表明，对于一般的问题，没有限制的团队规模，在多项式空间中运行的枚举算法不存在。
2018-03-12 cs.CC cs.LO
Enumerating Teams in First-Order Team Logics
我们开始研究一阶群逻辑中不同可满足性问题的枚举复杂性。由于我们的许多问题超出了DelP，我们使用了一个框架，用于硬枚举类似于多项式层次结构，这是最近推出的Creamusu等人。2019）。我们证明了在给定的一阶结构中枚举一个固定公式的所有满足队的问题对于依赖逻辑和独立逻辑的某些公式是DelNP-完全的。对于包含逻辑公式，这个问题甚至在DelP中也存在。此外，我们研究了这个问题的变种，只有最大，最小，最大和最小的解决方案，分别考虑。在大多数情况下，这些问题与原始问题具有相同的复杂性。一个例外是包含逻辑的最小变量，它是DelNP完全的。
2020-12-29 cs.LO
On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties
在这篇文章中，我们研究线性时态逻辑与团队语义（TeamLTL），是新的逻辑定义超属性。我们将这些逻辑的坎普型翻译定义为一阶团队逻辑和二阶逻辑的片段。我们还描述了团队逻辑和二阶逻辑的模型检查和可满足性的表达能力和复杂性，将它们与二阶和三阶算术联系起来。我们的结果集在一个更大的背景下，最近的结果Lück表明，扩展TeamLTL的布尔否定是高度不可判定的下，所谓的同步语义。我们还研究了TeamLTL扩展的口吃不变片段。
2021-10-21 cs.LO math.LO
Uniform Interpolation for Propositional and Modal Team Logics
在本文中，我们考虑模态组逻辑，经典模态逻辑的推广，它是可能的数据之间的依赖现象描述。我们证明，最有名的片段全模态团队逻辑允许消除所谓的“存在互模拟量词”，其中存在的某个集合是模互模拟。因此，我们证明了这些片段享有一致插值性质。
2018-10-12 cs.LO
Inductive Learning of Logical Theories with LLMs: An Expressivity-Graded Analysis
Idiap Research Institute（伊迪亚普研究所）；University of Manchester（曼彻斯特大学）
本研究提出结合形式化推理引擎反馈的分级分析方法，探究大语言模型在逻辑理论归纳任务中的能力边界，发现大模型可匹敌SOTA ILP系统，但长谓词关系链追踪比理论复杂度更具挑战。
2025-01-14 cs.AI cs.CL cs.LO
On the Complexity of Linear Temporal Logic with Team Semantics
在线性时序逻辑（LTL）中，一个以公式形式给出的规范通过一组迹来定义一个系统。然而，某些功能，如信息流的安全约束，而不是作为所谓的hyperproperties，这是一套套的痕迹。一种逻辑方法是团队逻辑，这是一个逻辑框架，用于规范信息的依赖性和独立性。团队语义的LTL最近被发现是超属性的逻辑。我们研究了具有同步团队语义和布尔否定的LTL的复杂性理论，证明了LTL的模型检验和可满足性问题都是高度不可判定的，等价于三阶算术的判定问题.此外，我们证明，这种复杂性已经出现在小的时间深度和只有“未来”模态F。最后，我们还介绍了口吃不变性的团队语义推广。
2020-04-27 cs.LO
Bisimulation and expressivity for conditional belief, degrees of belief, and safe belief
LORIA, CNRS / Université de Lorraine（洛里亚研究所、法国国家科学研究中心 / 洛林大学）；DTU Compute, Technical University of Denmark（丹麦技术大学计算学院）
可信性模型是Kripke模型，代理人使用它来推理他们自己和彼此的知识和信念。这些模型被用来解释条件信念、信念度和安全信念的概念。条件信念逻辑既包含该模态，也包含知识模态，信念度逻辑和安全信念逻辑也是如此。关于这些逻辑，可扩展性模型可能包含太多信息。需要一个适当的互模拟概念来表征它们。我们定义了互模拟的概念，并证明了所需的特征：类的图像有限和原像有限的模型（相对于可扩展性关系），两个指向Kripke模型是模态等价的三个逻辑中的任何一个，当且仅当它们是双相似的。结果，这种模型的信息内容可以类似地用条件信念逻辑、信念程度逻辑或安全信念逻辑来表示。我们发现了一个惊人的结果。然而，这并不意味着逻辑具有同样的表达性：条件和信念度的逻辑是不可比较的，信念度的逻辑和安全信念的逻辑是不可比较的，而安全信念的逻辑比条件信念的逻辑更具表达性。鉴于互模拟表征的结果，这是一个同样令人惊讶的结果。我们希望我们的见解可能有助于不断增长的社区正式认识论和定性和定量建模之间的关系。
2016-02-25 cs.AI cs.LO
Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality
均匀一维片段UF 1 ^=是从一阶逻辑中获得的一种形式，通过将量化限制在存在（全称）量词块的应用中，使得在量化公式中最多有一个变量保持自由。片段在布尔运算下是闭合的，但附加的限制（称为一致性条件）适用于具有两个或多个变量的原子公式的组合。这个片段可以被看作是二元逻辑的规范化推广，定义它是为了能够处理任意的关系。最近引入了分片的概念，并证明了UF 1 ^=的无等式分片的可满足性问题是可判定的.本文证明了UF 1 ^=的可满足性和有限可满足性问题是NEXPTIME-完全的。我们还证明了具有计数量词的扩展UF ^=的相应问题是不可判定的。除了可判定性问题，我们还比较了UF ^=和二元逻辑与计数量词FOC^2的表达性。我们表明，虽然逻辑一般来说是不可比较的，但当注意力仅限于元数界为二的词汇时，UF 1 ^=严格包含在FOC^2中。
2014-09-02 cs.LO math.LO
On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics
本文为存在二阶逻辑及团队语义逻辑的并闭片段提供语法刻画，引入包含-排除博弈作为模型检验博弈，并定义团队原子以精确捕获并闭片段，解答了开放问题。
2021-07-29 cs.LO
Time Window Temporal Logic
本文介绍了时间窗口时序逻辑（TWTL），一个丰富的表达能力的语言，用于描述各种时间有界规范。特别是，TWTL的语法和语义使串行任务的紧凑表示成为可能，这通常见于机器人和控制应用。本文还讨论了TWTL公式关于任务截止期的松弛问题。有效的自动机为基础的框架，以解决综合，验证和学习问题。所提出的解决方案的关键成分是一个算法，翻译一个TWTL公式的注释有限状态自动机，编码所有可能的时间松弛的规范。案例研究说明了表达的逻辑和提出的算法。
2016-02-13 cs.FL cs.LO
Logic and Computation through the Lens of Semirings
该研究在Grädel和Tannen提出的半环语义框架下，分析一阶逻辑及其扩展的表达与计算特性，通过推广的Blum-Shub-Smale机器和半环算术电路刻画其复杂度，并给出交换正半环上常深度算术电路的逻辑刻画。
2025-05-20 cs.CC cs.LO
Unifying approach to uniform expressivity of graph neural networks
School of Computer Science, University of Sheffield, UK（谢菲尔德大学计算机科学学院）；School of Computing Science, University of Glasgow, UK（格拉斯哥大学计算科学学院）
本文提出模板GNNs框架和Graded template modal logic逻辑，统一分析图神经网络的表达能力，并展示标准AC-GNNs及其变体作为T-GNNs的实例。
2026-02-20 cs.AI cs.LG cs.LO
On the Complexity of Team Logic and its Two-Variable Fragment
本文研究了具有团队语义的一阶逻辑的无限制布尔否定扩展--FO（~）逻辑。它最近被证明是可公理化的，但在计算复杂性的问题上还没有得到太多的关注。本文考虑它的二元片段FO 2（~），证明了它的可满足性问题是可判定的，并且对于最近引入的非初等类TOWER（poly）是完全的.此外，我们还对FO（~）的模型检验的复杂性进行了分类，并证明了PSPACE-完备性和ATIME-ALT（exp，poly）-完备性之间的二分法。为了实现下界，我们提出了从模态团队逻辑MTL到FO 2（~）的转换，该转换扩展了从模态逻辑ML到FO 2的众所周知的标准转换。对于上界，我们转换为二阶逻辑的一个片段。
2018-04-13 cs.LO
Soft lambda-calculus: a language for polynomial time computation
软线性逻辑（[Lafont02]）是线性逻辑的一个子系统，其特征是PTIME类。我们介绍软Aldida演算作为演算典型的直觉和仿射变体的这种逻辑。我们证明了该演算的（无类型）项可以在多项式时间内约简。然后，我们扩展了软逻辑的类型系统与递归类型。这允许我们考虑表示列表的非标准类型。利用这些数据集，我们以插入排序算法为例，检验了软微积分的具体表达能力。
2003-12-07 cs.CC cs.LO
Tractability Frontier of Data Complexity in Team Semantics
研究了具有团队语义的逻辑模型检测的数据复杂性。我们专注于严格和宽松的团队语义下的依赖，包含和独立逻辑公式。我们的研究结果描绘了一个清晰的易处理性/难处理性边界的数据复杂性的量化器的自由和量化的公式为每个逻辑。对于松散语义下的包含逻辑，我们将模型检测问题归结为所谓的双Horn布尔公式的可满足性问题。通过这种约简，我们给出了包含逻辑的数据复杂性在PTIME内的已知结果的另一种证明。
2021-08-12 cs.LO
A Van Benthem Theorem for Modal Team Semantics
著名的van Bentham定理指出模态逻辑恰好对应于在互模拟下不变的一阶逻辑的片段。在这篇文章中，我们证明了一个精确的模拟这个定理的框架中的模态依赖逻辑MDL和团队语义。我们表明，模态团队逻辑MTL，扩展MDL的经典否定，捕捉到的正是FO-可定义的互模拟不变性质的Kripke结构和团队。我们还比较了MTL的表达能力，最近在该地区研究的MDL的大多数变体和扩展。
2015-07-13 cs.LO
A Primer for Preferential Non-Monotonic Propositional Team Logics
FernUniversität in Hagen（哈根大学）；University of Helsinki（赫尔辛基大学）
该文在命题团队语义框架下研究KLM风格偏好非单调推理，证明团队命题逻辑可生成累积非单调后承，给出满足System P的命题依赖逻辑偏好模型的精确刻画，并说明经典及依赖逻辑后承的非平凡偏好模型表示方法。
2024-05-11 cs.AI cs.LO
On the Expressive Power of Inquisitive Team Logic and Inquisitive First-Order Logic
University of Helsinki（赫尔辛基大学）；University of Padua（帕多瓦大学）
本文证明探究团队逻辑中开放公式的表达能力严格超越一阶逻辑，并扩展至探究一阶逻辑，解决了一个开放问题。
2026-07-01 cs.LO math.LO
Labelled Sequent Calculi for Propositional Team Logics
University of Helsinki（赫尔辛基大学）；University of Amsterdam, University of Southern Denmark（阿姆斯特丹大学，南丹麦大学）；University of Bern（伯尔尼大学）；Utrecht University（乌得勒支大学）
为基于团队语义的四种逻辑（基本探究逻辑、命题直觉主义依赖逻辑及其张量析取扩展）提供了可靠且完备的带标签矢列演算，并证明了弱化、收缩和切割规则的可容许性，最后给出了带简化标签的终止证明搜索过程。
2026-07-01 cs.LO
Parametrised Complexity of Model Checking and Satisfiability in Propositional Dependence Logic
在本文中，我们开始在依赖逻辑领域的参数化复杂性的系统研究，发现它的起源于依赖逻辑的Väänänen从2007年。我们研究这个逻辑（PDL）的命题变体，并调查各种参数化相对于中央决策问题。PDL的模型检验问题是NP完全问题。本研究的主题是确定一个参数列表（公式大小，树宽，树深，团队规模，变量数）下MC成为固定参数易处理。此外，我们表明，析取的数量或依赖原子的arity（dep-arity）作为一个参数都产生paraNP-完全性的结果。然后，我们考虑的可满足性问题（SAT）显示出不同的图片：在团队规模，或deparity SAT是paraNP-完全的，而在所有其他提到的参数的问题是FPT。最后，我们介绍了一个变种的可满足性问题，要求一个给定的规模的团队，并显示这个问题的一个几乎完整的图片。
2020-06-13 cs.CC cs.LO
Polyteam Semantics
团队语义是现代依赖和独立逻辑的数学框架，其中公式由赋值集（团队）解释，而不是一阶逻辑中的单个赋值。为了加深团队语义和数据库依赖理论之间富有成效的相互作用，我们定义了“多队语义”，其中公式在一个家庭的团队进行评估。我们首先定义了一个新的polyteam变体的依赖原子，并给出了相关的蕴涵问题的有限axiomatisation。我们涉及多队语义的团队语义和调查的情况下，前者的逻辑可以模拟逻辑在后者。我们还通过存在二阶逻辑（ESO）中向下封闭和可定义的多队的性质来证明多依赖逻辑的表达能力。类似的结果是持有多独立逻辑和所有ESO定义的属性。我们还将多包含逻辑与最大不动点逻辑联系起来。
2020-03-26 cs.LO
There are (other) ways to negate in propositional team semantics
本文研究命题团队语义中的否定机制，证明完全直觉主义否定不增加向下封闭逻辑的公理化复杂度，并证明同时含依赖原子与包含原子的命题逻辑具有表达完备性。
2024-10-10 cs.LO math.LO
On elementary logics for quantitative dependencies
我们定义和研究的概率团队语义和超元有限结构的框架中的逻辑。我们的工作是最近发展的新的公理化和听话的逻辑团队语义下的布尔否定关闭。我们的逻辑采用新的概率原子，类似于所谓的扩展原子从团队语义文学。我们还定义了对应的我们的逻辑在亚有限结构，并表明我们所有的逻辑可以被翻译成功能不动点逻辑意味着一个多项式时间上界的BSS计算的数据复杂性。
2021-04-09 cs.LO
Characterising Modal Definability of Team-Based Logics via the Universal Modality
我们研究了各种模态逻辑的模型和框架可定义性。设ML（A+）表示用普适模态扩展的模态逻辑的片段，其中普适模态只肯定地出现。我们证明了一类Kripke模型在ML（A+）中是可定义的当且仅当该类是初等的，并且在不相交的工会和满射互模拟下是封闭的。我们还讨论了ML（A+）的可定义性的精神，著名的Goldblatt-Maxason定理。我们证明了Kripke框架的一个初等类F在ML（A+）中是可定义的当且仅当F在取生成子帧和有界形态图像下是闭的，并且反映了超滤子扩展和超滤子帧生成.此外，我们还研究了相对于有限传递框架的框架可定义性，并给出了相对于有限传递框架的ML（A+）-可定义性的一个类似刻画。最后，我们在团队逻辑中开始了模型和框架可定义性的研究。我们研究（扩展）模态依赖逻辑，（扩展）模态包含逻辑和模态团队逻辑。我们建立严格的线性层次模型的可定义性和框架的可定义性，分别。我们表明，关于模型和框架的可定义性，前面提到的团队为基础的逻辑，除了模态依赖逻辑，要么符合ML（A+）或平原模态逻辑ML。因此，作为一个推论，我们得到的模型和框架可定义的团队为基础的逻辑的模型论特征。
2018-02-21 cs.LO math.LO
Canonical Models and the Complexity of Modal Team Logic
该研究通过引入典范模型将模态团队逻辑MTL的可满足性简化为模型检验，并证明其复杂性为TOWER(poly)完全问题，同时刻画了有界模态深度片段的初等层级复杂性。
2019-04-10 cs.LO
Probabilistic team semantics
团队语义学是一个语义学框架，用于研究数据库和统计等许多领域中普遍存在的依赖和独立概念。在最近的作品团队语义已被概括，以适应也多集和概率依赖。在这篇文章中，我们研究了概率团队语义的一个变体，并将此框架与塔斯基双排序逻辑联系起来。我们还表明，我们的逻辑非常简单的量词自由公式引起NP难的模型检验问题。
2018-03-06 cs.LO
The Expressive Power of Modal Dependence Logic
我们研究了各种模态逻辑与团队语义的表达能力。我们表明，正是向下封闭和封闭下的团队k-互模拟的团队的属性，对于一些有限的k，是可定义的模态逻辑扩展与直觉析取。此外，我们还证明了直觉析取模态逻辑和扩展模态依赖逻辑的表达能力是一致的。最后，我们建立任何翻译从扩展模态依赖逻辑到模态逻辑与直觉析取增加一些公式的大小呈指数级。
2014-06-24 cs.LO math.LO
Logics with Multiteam Semantics
团队语义学是现代依赖与独立逻辑的数学基础。与经典的塔斯基语义相反，公式的求值不是针对自由变量的单个赋值，而是针对一组这样的赋值，称为组。团队语义适用于依赖概念的纯逻辑理解，其中只有数据的存在或不存在才重要，但基于集合，它不考虑数据值的多次出现。因此，在这种多重性很重要的情况下，特别是在推理概率和统计独立性方面，这是不够的。因此，一些作者提出了从团队到多团队（即多组分配）的扩展。在本文中，我们的目标是在多队语义的基础上，依赖和独立的逻辑系统的发展。我们研究原子依赖有限多队的属性，并讨论了适当的意义的逻辑运算符，以扩展原子的依赖关系，以充分成熟的逻辑推理的依赖属性在多队设置。我们探讨了各种不同的多队逻辑的属性和表达能力，并将它们与团队语义逻辑进行比较。我们还研究了逻辑与多队语义与存在二阶逻辑的关系，为一类特定的亚有限结构。事实证明，包含-排除逻辑可以在精确意义上由该逻辑的Presburger片段来表征，但是为了捕获独立性，我们需要超越它并添加某种形式的乘法。最后，我们还考虑了实数中的带权多队，并通过拓扑性质研究了公式的表达能力。
2020-11-19 cs.LO
A Double Team Semantics for Generalized Quantifiers
我们定义了基于双队的广义量词一阶逻辑的语义。我们还定义和研究了广义原子的概念。这样的原子可以用来定义具有基于团队的语义的一阶逻辑的扩展。我们还定义了一个游戏语义，并将其与双队语义进行了比较。
2017-08-31 cs.LO math.LO
The expressive power of modal logic with inclusion atoms
模态包含逻辑是基本模态逻辑的包含原子扩展，其语义定义在Kripke模型上。Kripke模型的团队只是其域的一个子集。本文给出了模态包含逻辑表达能力的一个完整刻画：一类带队的Kripke模型在模态包含逻辑中是可定义的当且仅当它在k-互模拟下是闭的，对于某个整数k，它在并下是闭的，并且它具有空队性质.我们还证明了同样的表达能力，可以通过添加一个单一的一元非空算子模态逻辑。此外，我们建立了一个指数下界的大小从模态包含逻辑到模态逻辑与非空算子的翻译。
2015-09-24 cs.LO math.LO
Modular SAT-based techniques for reasoning tasks in team semantics
我们研究了团队语义中逻辑推理任务的复杂性。我们的主要重点是数据的复杂性模型检验，但我们也得到了新的结果，逻辑定义的计数和枚举问题。我们的方法是基于这些问题的模块化减少到相应的问题的各类布尔公式。我们说明了我们的方法，通过几个新的易处理性/难处理性的结果。
2022-04-01 cs.LO
Complexity Results in Team Semantics: Nonemptiness Is Not So Complex
University of Helsinki（赫尔辛基大学）；Utrecht University（乌得勒支大学）
研究团队语义中凸逻辑的复杂性，针对带非空原子NE的经典命题逻辑扩展，证明可满足性问题是NP完全的，有效问题是coNP完全的，模型检验问题属于P。
2026-02-26 cs.LO math.LO
Model Checking and Validity in Propositional and Modal Inclusion Logics
命题包含逻辑和模态包含逻辑是属于基于团队语义的逻辑家族的形式主义。本文研究了这些逻辑的模型检验和有效性问题。我们确定这两个问题的复杂性界限，包括宽松和严格的团队语义。通过这样做，我们接近完成该计划，其最终目的是分类的中心推理问题的复杂性模态和命题依赖，独立性和包含逻辑。
2017-04-24 cs.LO
On the Complexity and Properties of Preferential Propositional Dependence Logic
Artificial Intelligence Group, University of Hagen（汉内斯大学人工智能小组）；Theoretical Computer Science, Leibniz University Hannover（汉诺威莱比锡大学理论计算机科学）；Department of Mathematics and Statistics, University of Helsinki（赫尔辛基大学数学与统计学系）
本文研究命题依赖逻辑中的 KLM 风格偏好推理，刻画其满足 System P 的条件，分析与团队命题逻辑的差异，并给出模型表示及两种表示下的复杂性结果。
2025-05-13 cs.AI cs.LO
