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
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
Enumeration Complexity of Poor Man's Propositional Dependence Logic
依赖逻辑（英语：Dependence logics）是一个现代的独立和依赖逻辑家族，模仿数据库理论的概念。本文旨在开创依赖逻辑领域中枚举复杂性的研究，从而对数据库查询答案的枚举问题提出一个新的观点。因此，作为第一步，我们调查的问题，枚举所有满足队的公式从一个给定的片段命题依赖逻辑。我们区分由任意函数限制团队规模和参数化版本，其中参数是团队规模。我们表明，多项式延迟可以达到多项式，否则在参数化设置，我们达到FPT延迟。然而，构造的具有多项式延迟的枚举算法需要指数空间。我们证明了一个增量多项式延迟算法存在，它只使用多项式空间。相反，我们表明，对于一般的问题，没有限制的团队规模，在多项式空间中运行的枚举算法不存在。
2018-03-12 cs.CC 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
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
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
Polyteam Semantics
团队语义是现代依赖和独立逻辑的数学框架，其中公式由赋值集（团队）解释，而不是一阶逻辑中的单个赋值。为了加深团队语义和数据库依赖理论之间富有成效的相互作用，我们定义了“多队语义”，其中公式在一个家庭的团队进行评估。我们首先定义了一个新的polyteam变体的依赖原子，并给出了相关的蕴涵问题的有限axiomatisation。我们涉及多队语义的团队语义和调查的情况下，前者的逻辑可以模拟逻辑在后者。我们还通过存在二阶逻辑（ESO）中向下封闭和可定义的多队的性质来证明多依赖逻辑的表达能力。类似的结果是持有多独立逻辑和所有ESO定义的属性。我们还将多包含逻辑与最大不动点逻辑联系起来。
2020-03-26 cs.LO
On elementary logics for quantitative dependencies
我们定义和研究的概率团队语义和超元有限结构的框架中的逻辑。我们的工作是最近发展的新的公理化和听话的逻辑团队语义下的布尔否定关闭。我们的逻辑采用新的概率原子，类似于所谓的扩展原子从团队语义文学。我们还定义了对应的我们的逻辑在亚有限结构，并表明我们所有的逻辑可以被翻译成功能不动点逻辑意味着一个多项式时间上界的BSS计算的数据复杂性。
2021-04-09 cs.LO
Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity
本文为异步 TeamLTL 提出基于集合的语义，研究布尔析取与布尔否定扩展，利用范式刻画其表达力与可判定性，并关联时间求值函数型异步逻辑。
2023-04-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
Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
研究了具有团队语义的模型检验线性时态逻辑（TeamLTL）的表达性和复杂性。TeamLTL，尽管是一个纯粹的模态逻辑，但能够定义超属性，即，与多个执行跟踪相关的属性。TeamLTL最近才被引入，关于它的表达能力和模型检验问题，只有很少的结果是已知的。我们将TeamLTL的表达性与通过用迹和命题量词（HyperLTL和HyperQPTL）扩展LTL获得的超性质的逻辑联系起来。通过这样做，我们得到了一些模型检验的TeamLTL结果，并确定其不可判定性边界。特别是，我们证明了任何向下封闭的TeamLTL扩展的所谓的左平坦片段的模型检验的可判定性。此外，我们建立了具有布尔析取和包含原子的TeamLTL的模型检验问题是不可判定的。
2021-11-23 cs.CC cs.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
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
Logics with Multiteam Semantics
团队语义学是现代依赖与独立逻辑的数学基础。与经典的塔斯基语义相反，公式的求值不是针对自由变量的单个赋值，而是针对一组这样的赋值，称为组。团队语义适用于依赖概念的纯逻辑理解，其中只有数据的存在或不存在才重要，但基于集合，它不考虑数据值的多次出现。因此，在这种多重性很重要的情况下，特别是在推理概率和统计独立性方面，这是不够的。因此，一些作者提出了从团队到多团队（即多组分配）的扩展。在本文中，我们的目标是在多队语义的基础上，依赖和独立的逻辑系统的发展。我们研究原子依赖有限多队的属性，并讨论了适当的意义的逻辑运算符，以扩展原子的依赖关系，以充分成熟的逻辑推理的依赖属性在多队设置。我们探讨了各种不同的多队逻辑的属性和表达能力，并将它们与团队语义逻辑进行比较。我们还研究了逻辑与多队语义与存在二阶逻辑的关系，为一类特定的亚有限结构。事实证明，包含-排除逻辑可以在精确意义上由该逻辑的Presburger片段来表征，但是为了捕获独立性，我们需要超越它并添加某种形式的乘法。最后，我们还考虑了实数中的带权多队，并通过拓扑性质研究了公式的表达能力。
2020-11-19 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
Logics with probabilistic team semantics and the Boolean negation
该研究针对带布尔否定的概率团队语义下的逻辑，分析了多类逻辑的表达能力关联，提出熵原子扩展一阶逻辑并验证其表达能力，还得到了相关逻辑问题的复杂度结果。
2024-05-22 cs.CC cs.LO
Modular SAT-based techniques for reasoning tasks in team semantics
我们研究了团队语义中逻辑推理任务的复杂性。我们的主要重点是数据的复杂性模型检验，但我们也得到了新的结果，逻辑定义的计数和枚举问题。我们的方法是基于这些问题的模块化减少到相应的问题的各类布尔公式。我们说明了我们的方法，通过几个新的易处理性/难处理性的结果。
2022-04-01 cs.LO
Model Checking and Validity in Propositional and Modal Inclusion Logics
命题包含逻辑和模态包含逻辑是属于基于团队语义的逻辑家族的形式主义。本文研究了这些逻辑的模型检验和有效性问题。我们确定这两个问题的复杂性界限，包括宽松和严格的团队语义。通过这样做，我们接近完成该计划，其最终目的是分类的中心推理问题的复杂性模态和命题依赖，独立性和包含逻辑。
2017-04-24 cs.LO
There are (other) ways to negate in propositional team semantics
本文研究命题团队语义中的否定机制，证明完全直觉主义否定不增加向下封闭逻辑的公理化复杂度，并证明同时含依赖原子与包含原子的命题逻辑具有表达完备性。
2024-10-10 cs.LO math.LO
Complexity of Propositional Logics in Team Semantics
我们分类的可满足性，有效性和模型检测问题的命题独立性，包含性和团队逻辑的计算复杂性。我们的主要结果表明，命题组逻辑的可满足性和有效性问题是完全的交替指数时间与多项式多交替。
2017-01-05 cs.CC cs.LO math.LO
Decidability of predicate logics with team semantics
我们研究了基于团队语义的谓词逻辑的复杂性。证明了二元独立逻辑和二元包含逻辑的可满足性问题都是NEXPTIME-完全的。此外，我们表明，两个变量的依赖逻辑的有效性问题是不可判定的，从而解决了一个开放的问题，从团队语义文献。我们还简要地分析了依赖逻辑的Bernays-Schönfinkel-Ramsey前缀类的复杂性。
2016-06-18 cs.CC cs.LO math.LO
On the Succinctness of Atoms of Dependency
本文通过引入公式大小博弈，系统比较了命题团队逻辑中各类非经典原子的简洁性，在存在片段中获得指数下界，在完整片段中获得多项式上界。
2019-08-19 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
The Expressive Power of Modal Dependence Logic
我们研究了各种模态逻辑与团队语义的表达能力。我们表明，正是向下封闭和封闭下的团队k-互模拟的团队的属性，对于一些有限的k，是可定义的模态逻辑扩展与直觉析取。此外，我们还证明了直觉析取模态逻辑和扩展模态依赖逻辑的表达能力是一致的。最后，我们建立任何翻译从扩展模态依赖逻辑到模态逻辑与直觉析取增加一些公式的大小呈指数级。
2014-06-24 cs.LO math.LO
Team Semantics for the Specification and Verification of Hyperproperties
我们开发团队语义的线性时序逻辑（LTL）来表达hyperproperties，这是最近被确定为一个关键的概念，在信息流属性的验证。从概念上讲，我们认为一个异步和同步的团队语义的变体。我们研究了这种新逻辑的基本性质，并对其可满足性、路径和模型检验问题的计算复杂性进行了分类。此外，我们将研究这些基本逻辑的扩展如何对添加其他原子运算符做出反应。最后，我们比较它的表现力的HyperLTL，另一个最近推出的逻辑hyperproperties。我们的研究结果表明，团队语义下的LTL是一个可行的替代HyperLTL，它补充了HyperLTL的表达能力，并具有部分更好的算法性能。
2018-06-25 cs.CC 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
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
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
Team Semantics and Recursive Enumerability
众所周知，依赖逻辑捕获复杂性类NP，最近已经表明，包含逻辑捕获有序模型上的P。这些结果表明，团队语义描述复杂性理论提供了有趣的新的可能性。为了正确理解团队语义和描述复杂性之间的联系，我们引入了依赖逻辑的扩展D*，它可以精确定义有限模型的所有递归可重复类。因此，D* 提供了一种替代图灵机的计算方法。D* 的基本新功能是一个运营商，可以扩展域所考虑的模型由有限数量的新鲜元素。由于广义量词与神谕之间的密切关系，我们也研究了广义量词在团队语义中的应用。我们证明了通过引入相应的广义依赖原子，可以从一阶逻辑的量词扩张中规范地消除（1）型单调量词。
2014-08-18 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
Dialetheism, Game Theoretic Semantics, and Paraconsistent Team Semantics
我们介绍了一个变体的依赖逻辑中的真理定义不存在的获胜策略的支持者（Eloise）在语义游戏中，但在缺乏获胜策略的对手（Abelard）。我们证明了这种语言是一阶逻辑的保守但次协调的扩展，它的有效性问题可以归结为一阶逻辑的有效性问题，它能够表达自己的真值和有效性谓词，并且它在表达上等价于通用二阶逻辑。此外，我们证明了一个次协调的非依赖逻辑公式是一致的当且仅当它是等价于一些一阶逻辑句子;另一方面，我们表明，所有的次协调依赖逻辑句子等价于一些一阶句子就真（但不一定就假）。
2014-03-14 cs.LO math.LO
A Parameterized View on the Complexity of Dependence Logic
本文研究了团队语义学领域中一种成熟的逻辑--依赖逻辑的模型检验的参数化复杂性。我们从这个问题的九个直接参数化的列表开始，即：分裂）/（自由）变量/全称量词，公式大小，输入结构的Gaifman图的树宽度，宇宙/团队的大小，以及依赖原子的arity。我们提出了一个全面的图片参数化的复杂性的模型检验，并获得了一个划分的问题，分为易处理和各种棘手的程度。此外，我们还考虑了复杂性的最重要的变量（数据和表达式的复杂性）的模型检验问题，通过固定部分的输入。
2021-09-20 cs.LO
Inclusion Logic and Fixed Point Logic
我们研究了包含逻辑的性质，即一阶逻辑与团队语义扩展包含依赖。本文证明了包含逻辑与最大不动点逻辑等价，并证明了关系的所有并闭一阶可定义性质在包含逻辑中都是可定义的，给出了包含逻辑的一个Escherichfeucht-Fraïssé对策，并举例说明了它的应用.
2013-04-30 cs.LO
Unified Foundations of Team Semantics via Semirings
一阶逻辑的半环语义提供了一种跟踪模型表示的事实如何用于推导公式满足的方法。团队语义学是一个框架，用于研究在数据库、量子力学和统计学等不同背景下的依赖和独立逻辑，通过用描述变量之间依赖关系的原子扩展一阶逻辑。结合这两个，我们提出了一个统一的方法，通过一个新的半环团队语义，它包含了所有以前考虑的一阶团队语义的变体的依赖和独立的概念进行分析。特别地，我们研究了不同半环之间依赖关系和公式满足的保持性。此外，我们还创建了推理任务的链接，如出处，计数和修复。
2023-03-14 cs.DB cs.LO
Bicompleteness Theorems for Team Logics with the Dual Negation
University of Padua（帕多瓦大学）
研究独立友好逻辑和依赖逻辑中双重否定的语义不确定性，通过调整不相容概念，为多种模态和命题团队逻辑建立了类似结果，并提出了关于不相容性的表达完备性概念。
2026-06-23 cs.LO math.LO
Safe Dependency Atoms and Possibility Operators in Team Semantics
我考虑的问题是，哪些依赖关系是安全的一个团队语义为基础的逻辑FO（D），在这个意义上，他们不增加其表达能力的句子时，添加到它。我表明，一些依赖关系，如整体，非恒定性和非空性，是安全的所有逻辑FO（D），和其他依赖关系，如恒定性，尽管是强一阶的，但对于D的某些选择，对于FO（D）是不安全的。我还证明了可能性算子，它在一个团队中成立，当且仅当它的参数在一些非空的子团队中成立，可以添加到任何逻辑FO（D），而不增加其对句子的表达能力。
2018-09-11 cs.LO math.LO
The Logic of Approximate Dependence
我们扩展处理的函数相关，依赖逻辑的基本概念，包括依赖的可能性与有限数量的例外。我们称之为近似依赖。本文的主要结果是近似依赖原子的完备性定理。我们指出了一些有问题的特点，这表明我们应该考虑多个团队，而不仅仅是团队。
2014-08-19 cs.LO math.LO
Structural Multi-type Sequent Calculus for Inquisitive Logic
本文定义了一种可靠的、完备的、具有Belnap式割消和子公式性质的多型演算。探究逻辑是探究语义的逻辑，由Groenendijk，Roelofsen和Ciardelli开发的语义框架，它捕获自然语言中的断言和问题。探究式逻辑是健全的，完整的。所谓的状态语义（也称为团队语义）。希尔伯特式的探究逻辑表示在一致替换下并不是封闭的;事实上，某些公式的出现被限制在公式的某个子类中，称为平坦公式。这一点和其他特征使得对这种逻辑的解析演算的探索并不简单。我们开发了一定的代数和秩序理论分析的团队语义，它提供了一个多类型的环境，占两个域的解释，平面和一般公式，以及它们的相互作用的设计准则。这种多类型的环境反过来又为我们在本文中介绍的查询逻辑的多类型演算提供了语义环境。
2016-04-04 cs.LO
Inquisitive Team Semantics of LTL
Pegaso University（佩加索大学）；University of Padua（帕多瓦大学）；CNRS, LIPN, Université Sorbonne Paris Nord（法国国家科学研究中心，LIPN，索邦巴黎北大学）；University of Napoli ``Federico II''（那不勒斯费德里科二世大学）
本文提出受探究逻辑启发的InqLTL团队语义，证明其带布尔否定时高度不可判定且表达力弱于带布尔否定的TeamLTL，同时找到一个可判定模型检验、可表达超性质的有意义片段。
2026-11-10 cs.FL cs.LO
A New Ehrenfeucht-Fraïssé Game for Dependence Logic
University College London（伦敦大学学院）；University of Helsinki（赫尔辛基大学）
针对依赖逻辑，提出一种基于单元素移动的新Ehrenfeucht-Fraïssé游戏，并证明其刻画了依赖逻辑中的初等等价性。
2026-05-30 cs.LO math.LO
Enumerating Minimal Unsatisfiable Cores of LTLf formulas
University of Calabria（卡拉布里亚大学）；University of Milano-Bicocca（米兰比可卡大学）
针对有限轨迹线性时序逻辑（LTLf）的不可行性解释需求，提出将LTLf公式编码为回答集编程（ASP）规范、利用ASP极小不可满足子集对应原公式极小不可满足核的枚举方法，在基准测试中取得良好性能。
2024-09-14 cs.AI cs.LO
Logics of Dependence and Independence: The Local Variants
现代的依赖和独立逻辑是基于团队语义的，这意味着公式的计算不是基于变量的单个赋值，而是基于一组这样的赋值，称为团队。这导致了存在二阶逻辑水平上的高表达能力。作为替代，Baltag和van Benthem提出了依赖逻辑的局部变体，称为函数依赖逻辑（logic of functional dependence，LFD）。虽然它的语义也是基于团队的，但公式只在其中一个分配上进行本地评估，并且团队只是作为评估过程中考虑的可能分配的供应。因此，这种逻辑依赖于广义赋值语义的模态视角，并且可以被看作是一阶逻辑的一个片段。对于不含等式的LFD变体，可满足性问题是可判定的。我们扩展了本地化逻辑的依赖和独立的想法，在一个系统的方式，考虑到本地变量的标准原子依赖属性：除了依赖和独立，还包括，排除和匿名。我们研究模型理论和算法问题的本地化逻辑，并解决了一些问题，已离开开放的巴尔塔格和范Benthem。特别地，我们研究了局部逻辑的可判定性问题，证明了等式可满足的LFD是不可判定的。此外，我们通过适当的互模拟的概念建立特征定理，并研究这些逻辑的模型检验问题的复杂性。
2021-02-20 cs.LO math.LO
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories
本文扩展算术语言刻画多项式时间随机函数，通过在逻辑系统内化误差界限检查，提出BPP的两种新刻画并引入可有效枚举子类BPP_T，最后证明多项式恒等式测试属于BPP_T。
2023-11-25 cs.LO math.LO
Upwards Closed Dependencies in Team Semantics
我们证明了，向上封闭的一阶依赖原子与团队语义的一阶逻辑不增加其表达能力（相对于句子），这同样是真的，如果我们还添加恒定原子。因此，函数相关、条件独立、包含和排除原子的否定都可以加入到一阶逻辑中，而不增加它的表达能力。此外，我们定义了一类有界向上封闭的依赖关系，我们证明了无界的依赖关系不能定义在有界的。
2013-07-17 cs.LO math.LO
Questions and dependency in intuitionistic logic
近年来，疑问句逻辑和依赖逻辑在探究逻辑和依赖逻辑两个密切相关的框架中得到了研究。这些研究假设经典逻辑作为陈述的背景逻辑，并在这个经典核心中加入了表达问题和依赖关系的公式。在本文中，我们通过在直觉主义逻辑的背景下研究问题和依赖关系来拓宽这些研究的范围。我们提出了一个直观的团队语义，团队嵌入在直观的Kripke模型。伴随逻辑是直觉主义逻辑的一个保守的扩展，带有问题和依赖公式。我们建立了一些关于这个逻辑的结果，包括一个范式的结果，一个完整性的结果，并翻译到经典的查询逻辑和模态依赖逻辑。
2017-04-06 cs.LO math.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
Representation Theorems for Cumulative Propositional Dependence Logics
Department of Mathematics and Statistics, University of Helsinki（赫尔辛基大学数学与统计学系）；Theoretical Computer Science, Leibniz University Hannover（汉诺威莱比锡大学理论计算机科学系）；Faculty of Mathematics and Computer Science, FernUniversität in Hagen（哈根应用科学大学数学与计算机科学学院）
本文研究了累积命题依赖逻辑和累积命题逻辑（具有团队语义）的表示定理，证明了其与特定模型的等价性，并为其他累积逻辑的表示定理提供了证明方法。
2026-02-24 cs.AI cs.LO
Complexity Thresholds in Inclusion Logic
具有团队语义的逻辑为复杂性类的逻辑表征提供了替代手段。依赖和独立逻辑都被认为可以捕获非确定性的多项式时间，并且这些逻辑中的易处理性的边界被相对较好地理解。包含逻辑类似于这些基于团队的逻辑形式主义，除了它对应于有序模型中的确定性多项式时间。在这篇文章中，我们研究包含逻辑的语法片段和不同的复杂性类之间的连接，在两个计算问题：最大的子组成员和模型检验问题的一个固定的包含逻辑公式。我们发现，非常简单的量词免费公式与一个或两个包含原子产生的这些问题是完整的（非确定性）对数空间和多项式时间的实例。此外，我们提出了一个片段的包含逻辑，捕捉非确定性的对数空间有序模型。
2019-03-26 cs.CC cs.DB cs.LO
Unifying Hidden-Variable Problems from Quantum Mechanics by Logics of Dependence and Independence
我们研究隐藏变量模型从量子力学，和他们的抽象在纯粹的概率和关系的框架，通过依赖和独立的逻辑，基于团队语义。我们发现，隐藏变量模型的共同理想的属性可以定义在一个优雅和简洁的方式在依赖和独立逻辑。不同性质之间的关系，以及它们的同时可实现性，因此可以在纯逻辑层面上被公式化和证明，作为逻辑公式的蕴涵和可满足性问题。在依赖和独立逻辑中，概率和关系蕴涵之间的联系使我们能够简化证明。在许多情况下，我们可以通过一个证明建立概率和关系隐变量模型的结果，因为一种情况意味着另一种情况，这取决于纯粹的语法标准。我们还讨论了贝尔和Kochen-Specker的不去定理，并提供了后者的一个纯粹的逻辑变体，引入非上下文选择作为一个团队语义属性。
2022-01-27 cs.LO math.LO
Bisimulation in Inquisitive Modal Logic
查询模态逻辑InqML是标准Kripke风格模态逻辑的推广。在它的认知化身中，它扩展了标准的认知逻辑，不仅可以捕获代理人拥有的信息，还可以捕获他们感兴趣的问题。从技术上讲，InqML属于基于团队语义的逻辑家族。从模型论的角度来看，它使我们在一元二阶逻辑的方向上迈出了一步，因为好奇的模态算子涉及世界集合上的量化。我们介绍和调查的互模拟等价的设置InqML的自然概念。我们比较了InqML和一阶逻辑的表达能力，并将InqML和一阶逻辑的互模拟不变片段作为一阶逻辑在各种两类关系结构上的互模拟不变片段。这些结果至关重要的是需要非经典的方法在研究互模拟和一阶的表现力在非小学类。
2017-07-27 cs.LO
