Aspects of Coherence in Dependence Logic
Leibniz Universität Hannover（汉诺威莱布尼茨大学）；University of Tartu（塔尔图大学）；University of Helsinki（赫尔辛基大学）；University of California Santa Cruz（加州大学圣克鲁兹分校）
本文研究依赖逻辑公式的k-相干性，证明无量词依赖逻辑公式的相干性等价于一阶可重写性，并分析了相干性判定问题的计算复杂性。
2026-05-29 cs.CC cs.LO
Dialectical logic: the Process Calculus
辩证逻辑是辩证过程的逻辑。辩证逻辑的目标是揭示逻辑计算系统中固有的动力学概念。标准逻辑中的命题和真值的基本概念被辩证逻辑中的过程和流的概念所包含。标准逻辑激发了辩证逻辑的核心顺序方面。Horn-clause逻辑要求类型和非对称性，也激发了辩证逻辑的平行方面。米尔纳和霍尔的过程逻辑揭示了辩证逻辑的内在和外在两个方面。辩证逻辑的序列内在方面应被看作是吉拉德线性逻辑的一种类型化或分布式的非对称张量形式。辩证逻辑的最简单版本本质上是直觉主义的。然而，通过遵循Glivenko在标准逻辑中使用双重否定闭包的方法，我们可以定义辩证逻辑的经典版本。
2018-10-09 cs.LO
A Fragment of Dependence Logic Capturing Polynomial Time
本文研究了Horn公式在依赖逻辑中的表达能力，证明了Horn公式可以表达NP完全问题。因此，我们定义了一个更小的片段D-Horn*，并表明，在有限的后继结构，它捕获的复杂性类P的所有集可判定的多项式时间。进一步研究了我们的结果是否可以推广到D-Horn* 的开公式和所谓的向下单调多项式时间性质的情形。
2014-09-03 cs.CC 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
Hierarchies in Dependence Logic
我们研究片段的依赖逻辑定义的全称量词或依赖原子的宽度限制的数量k的公式。我们发现存在二阶逻辑的子逻辑对应于依赖逻辑的这些片段。我们还表明，这两种方式定义片段的依赖逻辑产生了一个层次的表达能力相对于k。
2011-05-17 cs.LO
Boolean Dependence Logic and Partially-Ordered Connectives
我们介绍了一种新的依赖逻辑称为布尔依赖逻辑。在布尔依赖逻辑中，依赖原子的类型为=（x_1，...，x_n，α），其中α是布尔变量。直觉上，布尔依赖原子可以表示关系的量化，而标准依赖原子表示函数的量化。我们比较布尔依赖逻辑的表达能力依赖逻辑和一阶逻辑丰富的偏序连接词。我们证明了布尔依赖逻辑和依赖逻辑的表达能力是一致的。我们定义了自然的布尔依赖逻辑的语法片段，并表明，他们符合相应的片段的一阶逻辑丰富的偏序连接词的表达能力。然后，我们表明，片段形成一个严格的层次结构。
2014-06-27 cs.LO math.LO
Propositional Logics of Dependence
本文在命题层次上研究依赖逻辑。我们证明了几个有趣的命题依赖逻辑，包括命题依赖逻辑，命题直觉依赖逻辑以及命题查询逻辑，是表达完备的，并且具有析取或合取范式.我们提供了演绎系统，并证明了这些逻辑的完备性定理。
2016-03-07 cs.LO math.LO
Transition Semantics - The Dynamics of Dependence Logic
我们研究了依赖逻辑和博弈逻辑之间的关系。动态博弈逻辑的一个变种，称为过渡逻辑，开发，我们表明，它与依赖逻辑之间的关系是可比的一阶逻辑和动态博弈逻辑讨论的范Bentham。这表明了一个新的角度来解释依赖逻辑公式，在断言的可达性在游戏中的不完美的信息对自然。然后，我们利用这一直觉，通过开发依赖逻辑的表达等价变体，其中这种解释被带到前台。
2013-05-21 cs.LO math.LO
Axiomatizing Propositional Dependence Logics
通过扩展已有的命题逻辑和模态逻辑的公理化，给出了命题依赖逻辑（PD）、模态依赖逻辑（MDL）和扩展模态依赖逻辑（EMDL）的完备的希尔伯特式公理化.此外，我们给新的标记tableau演算PD，MDL，和EMDL。我们证明了每一个标记的结石的合理性，完整性和终止。
2014-10-19 cs.LO math.LO
Expressing Second-order Sentences in Intuitionistic Dependence Logic
直觉依赖逻辑由Abramsky和Vaananen（2009）引入，作为Hodges（trump）团队语义的一般结构下的依赖逻辑的变体。证明了从直觉依赖逻辑句子到二阶逻辑句子的转换。本文证明了另一个方向也成立，从而直觉依赖逻辑在句子层次上等价于二阶逻辑。
2013-02-09 cs.LO math.LO
A Simple Logic of Functional Dependence
本文提出了一个简单的可判定逻辑的功能依赖LFD，在经典命题逻辑的依赖原子和依赖量词作为模态处理的基础上，一阶逻辑的广义赋值语义的设置。探讨了LFD的表达强度、完备证明演算和元性质。各种语言扩展，以及，不可判定模态风格的独立性和动态逻辑的变化依赖模型。最后，更具体的设置相关性进行了讨论：连续依赖的拓扑模型，线性依赖的向量空间，时间依赖的动力系统和游戏。
2021-03-27 cs.LO math.LO
Complexity of Model Checking for Modal Dependence Logic
模态依赖逻辑（Modal Dependence Logic，MDL）是由Väänänen最近提出的。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n原子式=（p_1，...，p_（n-1），p_n）直观地说明p_n的值仅由p_1，.，p_（n-1）。我们证明了Kripke结构上MDL公式的模型检验是NP完全的，并进一步考虑了通过限制允许的命题和模态连接词的集合而得到的MDL片段。事实证明，几个片段，例如，没有情态动词或没有命题连接词的句子仍然是NP完全的。我们还考虑了MDL的限制，其中每个单个依赖原子的长度由整个逻辑固定的数字限制。我们表明，这个有界MDL的模型检验问题仍然是NP完全的。我们还通过允许经典析取（由Sevenster引入）来扩展MDL，除了依赖析取之外，并表明经典析取总是至少与有界元依赖原子一样糟糕，在某些情况下甚至更糟，例如，只有两个析取的片段是NP完全的。此外，我们几乎完全分类的计算复杂性的模型检验问题的所有限制的命题和模态算子的无界以及有界MDL。
2012-01-27 cs.CC cs.LO
Axiomatizing first order consequences in dependence logic
在[8]中引入的依赖逻辑不能被公理化。然而，依赖逻辑句子的一阶结果是可以公理化的，这就是本文要做的。我们给出了一个明确的公理化，并证明了相应的完备性定理。
2012-08-01 cs.LO math.LO
The Expressive Power of Modal Dependence Logic
我们研究了各种模态逻辑与团队语义的表达能力。我们表明，正是向下封闭和封闭下的团队k-互模拟的团队的属性，对于一些有限的k，是可定义的模态逻辑扩展与直觉析取。此外，我们还证明了直觉析取模态逻辑和扩展模态依赖逻辑的表达能力是一致的。最后，我们建立任何翻译从扩展模态依赖逻辑到模态逻辑与直觉析取增加一些公式的大小呈指数级。
2014-06-24 cs.LO math.LO
The Logic of Approximate Dependence
我们扩展处理的函数相关，依赖逻辑的基本概念，包括依赖的可能性与有限数量的例外。我们称之为近似依赖。本文的主要结果是近似依赖原子的完备性定理。我们指出了一些有问题的特点，这表明我们应该考虑多个团队，而不仅仅是团队。
2014-08-19 cs.LO math.LO
On Dependence Logic
我们给出了一个概述的依赖和独立逻辑的一些发展。这是一个小的选择，为新人，从一个快速增长的文学主题。进一步讨论了条件独立原子，证明了条件独立逻辑与非条件独立逻辑是等价的。最后，我们简要地讨论了我们的逻辑信念表示的应用。
2013-05-25 cs.LO math.LO
On Three-Valued Dependence-Like Logics
University of Lodz（罗兹大学）
本文探讨依赖逻辑与三值逻辑的关联，提出两种结合经典联结词与传染性联结词的三值依赖类逻辑，并给出相应的可靠完备无切割二叉相继式演算。
2026-10-07 cs.LO math.LO
The model checking problem for intuitionistic propositional logic with one variable is AC1-complete
我们证明了单变量直觉命题逻辑的模型检验问题对于对数空间一致AC 1是完备的。作为基本工具，我们使用直觉主义逻辑和海廷代数之间的联系，并探讨其复杂性的理论方面。对于单变量超直觉逻辑，我们得到了模型检验问题的NC 1-完全性。
2011-09-15 cs.CC cs.LO
Dependence logic with a majority quantifier
本文研究了有限结构上依赖逻辑D的择多量词M的扩张。我们表明，由此产生的逻辑是equi-expressive与二阶逻辑的扩展，由二阶多数量词的所有种族。我们的结果意味着，从描述复杂性理论的角度来看，D（M）捕获的复杂性类计数层次。
2013-03-08 cs.LO math.LO
Validity and Entailment in Modal and Propositional Dependence Logics
本文全面分类了模态与命题依赖逻辑中有效性与蕴涵的复杂性，证明模态依赖逻辑的有效性问题是NEXPTIME完全的，反驳了先前更高的复杂性猜想。
2019-04-25 cs.LO math.LO
Dependence Logic with Generalized Quantifiers: Axiomatizations
我们证明了两个完备性结果，一个是关于依赖逻辑由具有弱解释的单调广义量词Q扩展的结果，弱的意思是Q的解释随结构而变化。第二个结果考虑了依赖逻辑的扩展，其中Q被解释为“存在不可数的许多”。“这两个公理化都被证明是健全的，完整的FO（Q）的后果。
2013-04-02 cs.LO math.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
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
A Parameterized View on the Complexity of Dependence Logic
本文研究了团队语义学领域中一种成熟的逻辑--依赖逻辑的模型检验的参数化复杂性。我们从这个问题的九个直接参数化的列表开始，即：分裂）/（自由）变量/全称量词，公式大小，输入结构的Gaifman图的树宽度，宇宙/团队的大小，以及依赖原子的arity。我们提出了一个全面的图片参数化的复杂性的模型检验，并获得了一个划分的问题，分为易处理和各种棘手的程度。此外，我们还考虑了复杂性的最重要的变量（数据和表达式的复杂性）的模型检验问题，通过固定部分的输入。
2021-09-20 cs.LO
On the Complexity of Entailment for Cumulative Propositional Dependence Logics
University of Helsinki（赫尔辛基大学）
本文研究了累积命题依赖逻辑和累积命题逻辑（带有团队语义）的蕴含问题的复杂性，通过关系模型确定了其复杂性结果。
2026-05-20 cs.AI cs.LO
Unifying Hidden-Variable Problems from Quantum Mechanics by Logics of Dependence and Independence
我们研究隐藏变量模型从量子力学，和他们的抽象在纯粹的概率和关系的框架，通过依赖和独立的逻辑，基于团队语义。我们发现，隐藏变量模型的共同理想的属性可以定义在一个优雅和简洁的方式在依赖和独立逻辑。不同性质之间的关系，以及它们的同时可实现性，因此可以在纯逻辑层面上被公式化和证明，作为逻辑公式的蕴涵和可满足性问题。在依赖和独立逻辑中，概率和关系蕴涵之间的联系使我们能够简化证明。在许多情况下，我们可以通过一个证明建立概率和关系隐变量模型的结果，因为一种情况意味着另一种情况，这取决于纯粹的语法标准。我们还讨论了贝尔和Kochen-Specker的不去定理，并提供了后者的一个纯粹的逻辑变体，引入非上下文选择作为一个团队语义属性。
2022-01-27 cs.LO math.LO
Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free (full version)
线性时序逻辑（LTL）是反应式系统的标准规约语言，并成功地应用于工业环境。然而，许多缺点LTL已被确定在文献中，其中有限的表达，缺乏定量特征，无法表达鲁棒性。有克服这些缺点的工作，但其中每一个通常是孤立地解决。这对于所有缺点同时显现的应用是不够的。在这里，我们通过引入解决多个缺点的逻辑来解决这个问题。为此，我们结合逻辑线性动态逻辑，LTL，和强大的LTL，每个解决一个方面，新的逻辑。对于两个方面的所有组合，所得到的逻辑具有与普通LTL相同的期望算法属性。特别是，为LTL开发的高效算法后端也适用于这些新逻辑。最后，我们讨论如何同时解决这三个方面。
2021-04-29 cs.FL 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
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
Decidability of predicate logics with team semantics
我们研究了基于团队语义的谓词逻辑的复杂性。证明了二元独立逻辑和二元包含逻辑的可满足性问题都是NEXPTIME-完全的。此外，我们表明，两个变量的依赖逻辑的有效性问题是不可判定的，从而解决了一个开放的问题，从团队语义文献。我们还简要地分析了依赖逻辑的Bernays-Schönfinkel-Ramsey前缀类的复杂性。
2016-06-18 cs.CC 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
Logic and Computation through the Lens of Semirings
该研究在Grädel和Tannen提出的半环语义框架下，分析一阶逻辑及其扩展的表达与计算特性，通过推广的Blum-Shub-Smale机器和半环算术电路刻画其复杂度，并给出交换正半环上常深度算术电路的逻辑刻画。
2025-05-20 cs.CC cs.LO
Dependence Logics in Temporal Settings
本文通过扩展静态函数依赖的模态逻辑，研究动力系统中的时间依赖，提出并公理化了具有时间化变量、函数符号和下一时刻模态词的完备可判定逻辑，并展望其与更丰富时态逻辑及动态拓扑逻辑的结合。
2024-03-28 cs.LO math.LO
Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free
线性时序逻辑（LTL）是反应式系统的标准规约语言，并成功地应用于工业环境。然而，许多缺点LTL已被确定在文献中，其中有限的表达，缺乏定量特征，无法表达鲁棒性。有克服这些缺点的工作，但其中每一个通常是孤立地解决。这对于所有缺点同时显现的应用是不够的。在这里，我们通过引入解决多个缺点的逻辑来解决这个问题。为此，我们结合逻辑线性动态逻辑，LTL，和强大的LTL，每个解决一个方面，新的逻辑。对于两个方面的所有组合，所得到的逻辑具有与普通LTL相同的期望算法属性。特别是，为LTL开发的高效算法后端也适用于这些新逻辑。最后，我们讨论如何同时解决这三个方面。
2019-09-17 cs.FL cs.LO
Dependences in Strategy Logic
策略逻辑（SL）是一种非常有表现力的逻辑，用于指定和验证多智能体系统的属性：在SL中，人们可以量化策略，将它们分配给智能体，并表达结果的属性。这样一个强大的框架有两个缺点：第一，模型检验SL具有非初等的复杂性;第二，SL的确切语义是相当复杂的，可能不符合预期。在本文中，我们专注于SL的策略依赖，通过跟踪如何存在量化的策略在公式中可能（或可能不）取决于其他策略中选择的公式。我们研究了不同类型的依赖性，改进了[Mogavero等人，关于策略的推理：关于模型检查问题，2014]，并证明它们会产生不同的满意度关系。在设置策略可能只取决于他们所观察到的，我们确定了一个大的片段SL，我们证明模型检验可以在2 EXPTIME。
2017-08-19 cs.LO
A Separation Logic for Negative Dependence
关于基于散列的概率数据结构的形式化推理通常需要关于随机变量的推理，其中当一个变量变大时（例如散列到一个桶中的元素的数量），其他变量趋于变小（例如散列到其他桶中的元素的数量）。这是一个负相关的例子，它是概率独立性的推广，最近在算法设计和机器学习中发现了有趣的应用。尽管负相关对于概率数据结构的分析是有用的，但是现有的验证方法不能为随机化程序建立这种性质。为了填补这一空白，我们设计了LINA，概率分离逻辑推理负相关。继近年来概率分离逻辑利用分离合取推理随机变量的概率独立性之后，本文利用分离合取推理随机变量的负相关性。我们的断言逻辑具有两个分离的合取，一个用于独立，一个用于负依赖。本文将串蕴涵逻辑推广到支持多个分离连词，并给出了一个完善的证明系统。值得注意的是，用于分离合取的语义依赖于用于组合资源的非确定性操作，而不是部分操作。通过利用负依赖的闭包属性，我们的程序逻辑支持负依赖和单调操作的框架式规则。我们演示了如何LINA可以验证基于哈希的数据结构和balls-into-bin过程的概率属性。
2021-11-29 cs.LO cs.PL
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
可达性逻辑是一种形式主义，可用于表达迁移系统的部分正确性。在本文中，我们提出了三个证明系统的形式主义，所有这些都是健全的和完整的，并继承了共归纳逻辑的性质。然而，证明系统在几个方面有所不同。首先，他们使用归纳和共归纳的比例不同。第二个方面是组合性，广义上意味着它们能够在较小的系统上证明更简单的公式，并将这些公式作为引理重用于较大的系统上的更复杂的公式。第三方面是它们的合理性证明的困难。我们发现，更多的归纳证明系统的使用，更专业的是它的使用coinduction（相对于我们的问题域），更组成的证明系统，但更困难的合理性证明变得。我们还简要地介绍了这些结果在Isabelle/HOL和Coq证明助手的机制。
2019-09-04 cs.LO
On Quantified Propositional Logics and the Exponential Time Hierarchy
本文从复杂性理论的角度研究了量化命题逻辑。首先，我们引入交替依赖量化布尔公式（ADQBF），它推广了量化和依赖量化布尔公式。我们证明了ADQBF的真值评价是AEXPTIME（poly）-完全的。我们还确定片段的问题是完整的指数层次的水平。第二，我们研究命题的团队为基础的逻辑。我们表明，DQBF公式自然对应于量化命题依赖逻辑，并提出了一个一般的NEXPTIME上界量化命题逻辑与一大类广义依赖原子。此外，我们证明了AEXPTIME（多）-完备性命题队逻辑的扩展与广义依赖原子。
2016-09-14 cs.LO
Axiomatizations of Team Logics
在一个模块化的方法，我们提升希尔伯特式证明系统的命题，模态和一阶逻辑广义系统为各自的团队为基础的扩展。我们对Väänänen的一阶群逻辑TL的无依赖片段FO（~），命题群逻辑PTL，量化命题群逻辑QPTL，模态群逻辑MTL，以及相应的依赖、独立、包含和排除逻辑，得到了合理而完整的公理化.作为完备性证明的关键步骤，我们证明了上述逻辑在某种意义上承认从公式中消除模态和量词的语义保持性。
2018-03-26 cs.LO
Questions and dependency in intuitionistic logic
近年来，疑问句逻辑和依赖逻辑在探究逻辑和依赖逻辑两个密切相关的框架中得到了研究。这些研究假设经典逻辑作为陈述的背景逻辑，并在这个经典核心中加入了表达问题和依赖关系的公式。在本文中，我们通过在直觉主义逻辑的背景下研究问题和依赖关系来拓宽这些研究的范围。我们提出了一个直观的团队语义，团队嵌入在直观的Kripke模型。伴随逻辑是直觉主义逻辑的一个保守的扩展，带有问题和依赖公式。我们建立了一些关于这个逻辑的结果，包括一个范式的结果，一个完整性的结果，并翻译到经典的查询逻辑和模态依赖逻辑。
2017-04-06 cs.LO math.LO
First-Order Modal $ξ$-Calculus: On the Aspects of Application and Bisimulation
本文提出了一阶模态$ξ$ -演算以及系谱Kripke模型。受模态$μ$ -演算的启发，一阶模态$ξ$ -演算采取了非常相似的形式，并将其归纳表达扩展到不同的维度。我们阐述了几个生动的例子，证明了这种逻辑的深刻的效用，特别是描绘家谱的并发计算机进程。互模拟概念的逻辑也得到了彻底的检查。
2023-01-17 cs.LO math.LO
Comparing several calculi for first-order infinite-valued Łukasiewicz logic
从可证明性的观点出发，比较了一阶无穷值Pukasiewicz逻辑和一阶有理Pavelka逻辑的Gentzen型超代数演算，并与Hájek的Hilbert型演算进行了比较.我们的比较的关键方面是密度消除证明的hypereclipse结石之一。
2018-12-13 cs.LO
Polyteam Semantics
团队语义是现代依赖和独立逻辑的数学框架，其中公式由赋值集（团队）解释，而不是一阶逻辑中的单个赋值。为了加深团队语义和数据库依赖理论之间富有成效的相互作用，我们定义了“多队语义”，其中公式在一个家庭的团队进行评估。我们首先定义了一个新的polyteam变体的依赖原子，并给出了相关的蕴涵问题的有限axiomatisation。我们涉及多队语义的团队语义和调查的情况下，前者的逻辑可以模拟逻辑在后者。我们还通过存在二阶逻辑（ESO）中向下封闭和可定义的多队的性质来证明多依赖逻辑的表达能力。类似的结果是持有多独立逻辑和所有ESO定义的属性。我们还将多包含逻辑与最大不动点逻辑联系起来。
2020-03-26 cs.LO
Dependence and Independence
我们引入一个原子公式直观地说，给定的变量是独立于给定的其他变量，如果第三组变量保持不变。我们将其与依赖逻辑进行对比。我们表明，我们的独立原子产生了一个自然的逻辑能够形式化的基本直觉的独立性和依赖性。
2012-08-27 cs.LO math.LO
Extending Urban Multi-Lane Spatial Logic to Formalise Road Junction Rules
在自动驾驶汽车（AV）的设计过程中，有几个阶段应该包括验证过程，以确保AV在道路上安全行驶。其中一个阶段是确保自动驾驶汽车遵守道路交通规则。为了将道路交通规则包括在AV的设计中，需要对这些规则进行精确和明确的形式化。然而，直到最近，这已经被指出为AV设计的一个问题，并且关于这一点的少数工作仅捕获规则的时间方面，而将空间方面抛在后面。在这里，我们扩展的空间交通逻辑，城市多车道的空间逻辑，正式的英国路口规则，在时间和空间方面的规则被捕获的一个子集。我们的方法有一个抽象的城市路口，可以很容易地促进正式的整套路口规则，我们示范正式的英国路口规则。一旦我们正式确定了整套标准，我们将根据道路交通规则对自动驾驶汽车的行为进行建模、实施和正式验证，以便为自动驾驶汽车制定数字公路代码的指导方针。
2021-10-25 cs.LO
Local Dependence and Guarding
我们研究了Baltag和van Bentham（2021）提出的函数依赖的基逻辑LFD及其与一阶逻辑的保护片段GF的关系。与其他依赖逻辑一样，LFD的语义使用团队：允许的变量赋值集。LFD的与众不同之处在于它能够表达变量之间的局部依赖关系和语句对变量的局部依赖关系。LFD的已知特征包括可判定性、显式公理化、有限模型属性和互模拟特性。其他问题，包括可满足性的复杂性问题，迄今为止仍然没有定论。更一般地说，一直缺乏的是一个很好的理解是什么使LFD方法依赖计算良好的行为，以及它如何与其他可判定逻辑。特别是，允许变量依赖和保护量词作为逻辑设备如何比较？我们提供了一个新的合成翻译从GF到LFD，相反，我们翻译LFD到GF中的“几乎合成”的方式。使用这两个平移，我们以统一的方式将关于GF的已知结果转移到LFD，例如，LFD可满足性以及Craig插值的严格复杂性界限。相反，例如，LFD的有限模型性质转移到GF。因此，局部依赖和局部保护是一个错综复杂的概念。
2022-06-13 cs.LO math.LO
Contextual Semantics: From Quantum Mechanics to Logic, Databases, Constraints, and Complexity
我们讨论量子非局部性和上下文，强调逻辑和结构方面。我们还展示了相同的数学结构如何出现在经典计算的各个领域。
2014-06-28 cs.LO quant-ph
Complete Additivity and Modal Incompleteness
在本文中，我们讲述了一个关于模态逻辑中不完备性的故事。这个故事编织在一起的文件范Bentham，“句法方面的模态不完备性定理，”和一个长期悬而未决的问题：是否每个正常的模态逻辑可以由一类完全加性模态代数，或我们称之为，V-BAO。使用一阶的完全可加性的性质的重新表述，我们证明了模态逻辑，主演的范Bentham的文件解决了开放的问题，在否定的。此外，对于双峰逻辑的情况下，我们表明，有一个自然发生的逻辑是不完整的V-BAO，即可证明性逻辑GLB。我们还表明，即使是不健全的逻辑，就这样的代数不一定要比经典的命题演算更复杂。另一方面，我们观察到，它是不可判定的语法定义的逻辑是否是V-完全的。在这些结果之后，我们将Blok二分法推广到V-不完全度。最后，我们回到van Bentham的主题，模态不完全性的句法方面。
2019-06-15 cs.LO
Complexity of Non-Monotonic Logics
Leibniz Universität Hannover（汉诺威莱布尼茨大学）
在过去的几十年中，非单调推理已经发展成为计算逻辑和人工智能领域的重要研究课题之一。已经考虑了将非单调方面引入经典逻辑的不同方式，例如，具有缺省规则的扩展、具有模态置信算子的扩展或语义的修改。在这个调查中，我们认为从上述每一种可能性的逻辑形式主义，即赖特的默认逻辑，摩尔的自我认知逻辑和麦卡锡的界限。此外，我们考虑溯因，其中一个是不感兴趣的推理，从一个给定的知识库，但在计算可能的解释观察相对于一个给定的知识库。这些逻辑的命题变体的不同推理任务的复杂性结果已经在90年代进行了研究。然而，近年来，可以观察到对复杂性问题的新的兴趣。一个当前的焦点方法是考虑参数化的问题，并确定合理的参数，允许FPT算法。在另一种方法中，重点在于识别片段，即，限制的逻辑语言，允许更有效的算法，最重要的推理任务。在本调查中，我们重点关注第二个方面。我们描述了通过限制允许的运算符集（例如，禁止否定，可以只考虑单调公式）或只考虑合取范式但具有广义子句类型的公式。我们考虑的算法问题是每个逻辑中的可满足性和蕴涵的合适变体，但也是计数问题，其中人们不仅对某些对象的存在感兴趣（例如，一个公式的模型），但要求他们的号码。
2010-09-10 cs.AI cs.CC cs.LO
Logics with Multiteam Semantics
团队语义学是现代依赖与独立逻辑的数学基础。与经典的塔斯基语义相反，公式的求值不是针对自由变量的单个赋值，而是针对一组这样的赋值，称为组。团队语义适用于依赖概念的纯逻辑理解，其中只有数据的存在或不存在才重要，但基于集合，它不考虑数据值的多次出现。因此，在这种多重性很重要的情况下，特别是在推理概率和统计独立性方面，这是不够的。因此，一些作者提出了从团队到多团队（即多组分配）的扩展。在本文中，我们的目标是在多队语义的基础上，依赖和独立的逻辑系统的发展。我们研究原子依赖有限多队的属性，并讨论了适当的意义的逻辑运算符，以扩展原子的依赖关系，以充分成熟的逻辑推理的依赖属性在多队设置。我们探讨了各种不同的多队逻辑的属性和表达能力，并将它们与团队语义逻辑进行比较。我们还研究了逻辑与多队语义与存在二阶逻辑的关系，为一类特定的亚有限结构。事实证明，包含-排除逻辑可以在精确意义上由该逻辑的Presburger片段来表征，但是为了捕获独立性，我们需要超越它并添加某种形式的乘法。最后，我们还考虑了实数中的带权多队，并通过拓扑性质研究了公式的表达能力。
2020-11-19 cs.LO
A New Execution Model for the logic of hereditary Harrop formulas
一类一阶遗传Harrop公式（$fohh$）是一阶Horn子句的一个良好扩展.它的操作语义是基于直觉可证明性的。我们提出了另一种操作语义的$fohh$，这是基于游戏语义。这个新语义有几个有趣的方面：特别是，它为Prolog中的$read$谓词提供了逻辑状态。
2015-07-07 cs.LO
Dialetheism, Game Theoretic Semantics, and Paraconsistent Team Semantics
我们介绍了一个变体的依赖逻辑中的真理定义不存在的获胜策略的支持者（Eloise）在语义游戏中，但在缺乏获胜策略的对手（Abelard）。我们证明了这种语言是一阶逻辑的保守但次协调的扩展，它的有效性问题可以归结为一阶逻辑的有效性问题，它能够表达自己的真值和有效性谓词，并且它在表达上等价于通用二阶逻辑。此外，我们证明了一个次协调的非依赖逻辑公式是一致的当且仅当它是等价于一些一阶逻辑句子;另一方面，我们表明，所有的次协调依赖逻辑句子等价于一些一阶句子就真（但不一定就假）。
2014-03-14 cs.LO math.LO
Indicative Conditionals and Dynamic Epistemic Logic
形式语义学中关于认知情态动词和指示条件句的最新观点与模态逻辑和动态认知逻辑中的观点有很大的重叠。本文的目的是展示如何更大的形式语义学和动态认知逻辑在这一领域之间的互动可以是互惠互利的。在一个方向上，我们展示了如何从模态逻辑和动态认知逻辑的概念和工具，可以用来给一个简单的，完整的公理化的Yalcin的[16]语义后果关系的语言与认知模态和指示条件。在另一个方向，由于Kolodny和MacFarlane [9]，指示条件的形式语义产生了一个新的动态算子，从动态认知逻辑的角度来看，它非常自然，允许简洁地表达依赖（如依赖逻辑）或附带陈述。我们证明了可判定性的逻辑与认知模态和Kolodny和MacFarlane的指示条件通过一个完整的和忠实的可计算的翻译从他们的逻辑模态逻辑K45。
2017-07-27 cs.LO
Finite Model Property and Bisimulation for LFD
最近，Baltag和van Benthem arXiv：2103.14946 [cs.LO]引入了一种新的具有局部依赖公式和依赖量词的函数依赖（LFD）可判定逻辑。该语言在依赖模型上进行解释，依赖模型是具有一组可用变量分配的一阶结构对，也称为团队。与依赖模型相关的团队可以被看作是一个标记的转换系统，在这个系统上LFD成为模态逻辑，其中依赖量词成为模态，局部依赖公式被视为特殊原子。在本文中，我们引入适当的互模拟的概念，将LFD（和一些相关的逻辑）表征为一阶逻辑（FOL）的一个片段，并表明它等价于arXiv：2102.10368 [cs.LO]中提出的更标准的互模拟概念，但对于互相似性检查更有效。我们的主要结果是LFD具有有限模型性质（FMP），通过Herwig定理的一个新的应用扩展部分同构。
2021-07-13 cs.LO math.LO
