The Complexity of Reasoning for Fragments of Autoepistemic Logic
自认知逻辑通过模态算子L扩展命题逻辑。前面有L的公式被称为“相信”。该逻辑由Moore在1985年引入，用于对理想理性主体的行为和对自己信念的推理进行建模。本文分析了自认知逻辑中所有布尔片断的三个最常见的决策问题--扩展存在、勇敢推理和谨慎推理的计算复杂性。作为第二个贡献，我们分类的计算复杂性计数的数量稳定的扩展一个给定的知识库。据我们所知，这是第一篇分析自认知逻辑计数问题的论文。
2010-06-01 cs.CC cs.LO
On the Complexity of Elementary Modal Logics
模态逻辑在计算机科学中有着广泛的应用。自20世纪70年代以来，模态可满足性问题的复杂性一直在研究，通常是在逐个案例的基础上证明结果。我们证明了一个非常普遍的分类广泛的一类相关的逻辑：模态逻辑的许多重要的子类可以通过限制允许的模型与一阶霍恩公式。我们证明了这些逻辑的可满足性问题是NP完全的或PSPACE困难的，并展示了一个简单的分类标准。此外，我们证明了许多PSPACE硬逻辑匹配的PSPACE上界。
2008-02-13 cs.CC cs.LO
The Complexity of Satisfiability in Non-Iterated and Iterated Probabilistic Logics
设L是经典命题逻辑的某种扩展。L上的非迭代概率逻辑是通过在L语言中添加非嵌套概率算子而定义的逻辑PL。例如，在PL中，我们可以表达这样的陈述“A的真实性概率为0.3”，其中A是L的公式。L上的迭代概率逻辑是逻辑PPL，其中概率运算符可以迭代（嵌套）。例如，在PPL中，我们可以表达这样的语句“这枚硬币是伪造的概率为0.6”。本文研究了概率算子对PL和PPL中可满足性复杂性的影响，得到了上述可满足性问题的复杂性界，该复杂性界是以既没有概率算子也没有经典算子作为顶连接符的正负公式的合取可满足性复杂性为参数的.作为我们的结果的应用，我们得到了紧的复杂性界的可满足性问题在PL和PPL时，L是经典的命题逻辑或理由逻辑。
2019-02-10 cs.CC cs.LO
Computational Complexity of Deciding Provability in Linear Logic and its Fragments
线性逻辑由Girard于1987年提出，与经典逻辑不同，它限制了弱化和收缩的结构推理规则的使用。这样，逻辑的原子就不再被解释为真理，而是被解释为信息或资源。这种解释使得线性逻辑成为数学和计算机科学中形式化的有用工具。例如，线性逻辑在证明论、量子逻辑和程序设计语言理论中得到了应用。逻辑的一个中心问题是一个给定的公式列表是否可以用微积分证明。在对这一问题复杂性的研究中，取得了一定的成果，但也存在一些问题。为了提出这些问题，并给出新的观点，本文由三个主要部分组成，它们相互建立：我们提出了语法，证明理论，和各种方法的语义线性逻辑。在这里，我们将遇到一些开放的研究问题。我们目前的状态复杂性理论表征的最重要的片段的线性逻辑。在这里，提出了进一步的研究问题，很明显，到目前为止，结果都使用了不同的方法。我们证明了一个原始的复杂性表征的逻辑片段，并提出了一个新的，结构性的方法来检查线性逻辑的可证明性的想法。
2021-09-28 cs.CC cs.LO
Complexity of two-variable Dependence Logic and IF-Logic
我们研究了依赖逻辑和独立友好逻辑的双变量片段D^2和IF^2。我们考虑了这些逻辑的可满足性和有限可满足性问题，并证明了对于D^2，这两个问题都是NEXPTIME-完全的，而对于IF^2，这两个问题是不可判定的。我们还证明了D^2的表达性严格低于IF^2，并且在D^2中已经可以表达两个一元谓词的等价性和无穷大（后者在存在常数符号的情况下）。这是第26届IEEE计算机科学逻辑研讨会（LICS 2011）会议录中出版物的扩展版本。
2011-04-15 cs.CC cs.LO
Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic
从计算复杂性的角度研究了分支时间逻辑CTL的可满足性问题。严格的上限和下限提供了每个时间操作符片段。在平行，最小模型的大小进行了研究，一个合适的概念极小。第三，研究了平坦的CTL，即，时态运算符嵌套深度非常低的公式。在复杂性和最小模型方面显示出尖锐的二分法：时间深度1具有低表达能力，而时间深度2相当于完整的CTL。
2017-02-24 cs.CC cs.LO
Closing a Gap in the Complexity of Refinement Modal Logic
精化模态逻辑（Refinement Modal Logic，RML），最近由Bozzelli等人提出，模态逻辑是经典模态逻辑的扩展，它允许人们对变化的模型进行推理。在本文中，我们研究与此逻辑相关的计算复杂性问题，解决了许多悬而未决的问题。具体来说，我们研究的复杂性，满足性的存在片段的RML，Bozzelli，范Ditmarsch和Pinchinat提出的问题。我们的主要结果是一个紧PSPACE上界这个问题，我们通过引入一个新的表系统实现。作为一个直接的后果，我们得到了严格的表征的复杂性RML可满足的任何固定数量的交替的细化量词。此外，通过一个简单的减少，我们建立RML的模型检验问题是PSPACE完全的，即使是一个单一的量词的公式。
2013-09-20 cs.CC cs.LO
Complexity Thresholds in Inclusion Logic
具有团队语义的逻辑为复杂性类的逻辑表征提供了替代手段。依赖和独立逻辑都被认为可以捕获非确定性的多项式时间，并且这些逻辑中的易处理性的边界被相对较好地理解。包含逻辑类似于这些基于团队的逻辑形式主义，除了它对应于有序模型中的确定性多项式时间。在这篇文章中，我们研究包含逻辑的语法片段和不同的复杂性类之间的连接，在两个计算问题：最大的子组成员和模型检验问题的一个固定的包含逻辑公式。我们发现，非常简单的量词免费公式与一个或两个包含原子产生的这些问题是完整的（非确定性）对数空间和多项式时间的实例。此外，我们提出了一个片段的包含逻辑，捕捉非确定性的对数空间有序模型。
2019-03-26 cs.CC cs.DB cs.LO
The Complexity of Reasoning for Fragments of Default Logic
缺省逻辑是由Reiter在1980年提出的。1992年Gottlob将命题缺省逻辑的延拓存在问题的复杂性分类为$\SigmaPtwo$ -完全问题，将轻信和怀疑推理问题的复杂性分类为SigmaP 2-完全问题。PiP 2-完成。此外，他还研究了默认规则的限制，即，半正常默认规则。Selman在1992年提出了类似的方法，使用了无析取和一元缺省规则。本文系统地限定了允许命题连接词的集合。我们给出了一个完整的复杂性分类的所有集合的布尔函数的Post格的意义上的所有三个常见的决策问题的命题缺省逻辑。我们表明，复杂性是一个hexachotomy（SigmaP 2-，DeltaP 2-，NP-，P-，NL-完全，平凡）的扩展存在问题，而对于轻信和怀疑推理问题，我们得到类似的分类没有平凡的情况。
2010-08-23 cs.CC cs.LO
Complexity of Propositional Logics in Team Semantics
我们分类的可满足性，有效性和模型检测问题的命题独立性，包含性和团队逻辑的计算复杂性。我们的主要结果表明，命题组逻辑的可满足性和有效性问题是完全的交替指数时间与多项式多交替。
2017-01-05 cs.CC cs.LO math.LO
A Parameterized Complexity View on Description Logic Reasoning
Institute for Logic, Language and Computation（逻辑、语言与计算研究所）；University of Amsterdam（阿姆斯特丹大学）
描述逻辑是一种知识表示语言，它被设计成在表达性和计算易处理性之间取得平衡。许多不同的描述逻辑已经被开发出来，并且这些逻辑的许多计算问题由于它们的计算复杂性而被研究。然而，基本上所有的复杂性分析的推理问题的描述逻辑使用的经典复杂性理论的一维框架。参数化复杂性理论的多维框架能够提供推理问题复杂性的更详细的图像。在本文中，我们认为，参数化复杂性的框架有很多可以提供的描述逻辑推理问题的复杂性分析-当一个人需要一个渐进的和前瞻性的观点参数化的复杂性工具。我们通过三个案例研究来证实我们的论点。第一个案例研究的问题是概念可满足的逻辑ALC关于近无环的TBox。第二个案例研究关注ALC概念的可满足性，其参数由联合算子的出现次数和完全存在量化的出现次数来确定。第三个案例研究从参数化复杂性的角度对数据复杂性结果进行了批判性的审视。这三个案例研究代表了描述逻辑问题的参数化复杂性方法的广泛应用。
2018-08-11 cs.AI cs.CC cs.LO
Logics for complexity classes
给出了图灵归约完备问题的一个新的句法刻画。一般的标准形式的发展，以定义这样的问题。其中一种形式允许我们在有序结构上定义完整的问题，另一种形式允许我们在无序的非阿斯特丽德结构上定义它们。使用规范形式，逻辑开发的各种复杂性类的完整的问题。证据表明，不可能有任何完整的问题，对几个复杂性类的阿斯特丽德结构。我们的方法是超越完整的问题。使用类似的形式，开发一个逻辑来捕获复杂性类$NP\cap coNP$，它很可能不包含完整的问题。
2014-09-29 cs.CC cs.LO
The complexity of positive first-order logic without equality
本文研究了在固定的有限结构B上求一阶逻辑无正等同性语句的复杂性。这可以被看作是非均匀量化的约束满足问题QCSP（B）的自然推广。我们引入满射超自同态，并使用它们来证明一个伽罗瓦连接，其特征在于可定义的正等式自由FO。通过代数方法，我们得出一个完整的复杂性分类为我们的问题B范围的大小最多为3的结构。具体来说，每个问题要么是在对数空间中，要么是NP完全的，要么是共NP完全的，要么是P空间完全的。
2010-03-03 cs.CC cs.LO
On the Parameterized Complexity of Default Logic and Autoepistemic Logic
Universität Hannover（汉诺威大学）；Université de la Méditerranée（地中海大学）；TWT GmbH（TWT有限公司）
本文研究了Courcelle定理和Elberfeld等人的对数空间形式的应用。在命题公式集的蕴涵问题、缺省逻辑的扩张存在问题以及自认知逻辑的扩张存在问题的背景下，得到了这些问题的固定参数时空有效算法.另一方面，我们展示，对于上述每个问题，一个非常简单的结构，对于广泛的不同的参数化，没有有效的固定参数算法（即使在大类XPnu的意义上）的实例的家庭，除非P=NP。
2011-10-06 cs.AI cs.CC
On the Parameterized Complexity of Graph Modification to First-Order Logic Properties
我们考虑的问题，决定是否可以修改输入图删除/添加最多k个顶点/边，使修改的结果满足一些属性定义在一阶逻辑。我们建立了一个充分必要条件的量化模式的一阶公式的固定参数易处理的问题或允许一个多项式核。
2019-02-26 cs.CC cs.DS
Data Complexity and Rewritability of Ontology-Mediated Queries in Metric Temporal Logic under the Event-Based Semantics (Full Version)
Birkbeck, University of London（伦敦大学伯贝克学院）；University of Oxford（牛津大学）；University of Warsaw（华沙大学）
我们调查的数据复杂性的基于事件的语义下，假设数据实例是有限时间的字时间戳与二进制分数的度量时态逻辑本体介导的回答查询。我们确定类的本体介导的查询回答，可以在AC0，NC1，L，NL，P，和coNP的数据复杂性，提供他们的重写一阶逻辑及其扩展与原始递归，传递闭包或databases，并建立较低的复杂性界限。
2019-07-01 cs.AI 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
The Complexity of Poor Man's Logic
受描述逻辑的启发，我们研究了如果我们只允许从字面量、$\wedge$、$\Diamond$和$\Box$构建公式，模态可满足性问题的复杂性会发生什么。以前，唯一已知的结果是K的可满足性问题的复杂性从PSPACE完全下降到coNP完全（Schmidt-Schauss和Smolka，1991和Donini等人，1992年）。在本文中，我们表明，不是所有的模态逻辑的行为像K。特别是，我们表明，可满足性问题的复杂性，其中每个世界至少有一个继任者的帧下降PSPACE-完整的P，但相比之下，可满足性问题的类的帧中，每个世界最多有两个继任者仍然PSPACE-完整的。作为后者的结果的推论，我们也解决了开放的问题，从Donini等人。描述逻辑的复杂性分类（Donini等人，1997年）。在最后一节中，我们对K的可满足性问题的复杂性进行了分类，对于算子集的所有其他限制。
2005-12-24 cs.CC cs.LO
The Complexity of Satisfiability for Fragments of Hybrid Logic -- Part I
混合逻辑的可满足性问题是不可判定的。这引发了一个关于可判定和可处理片段的研究计划。在本文中，我们调查的影响，限制命题部分的语言的可判定性和可满足性问题的复杂性在任意的，传递的，总的框架，框架的基础上的等价关系。我们还考虑了不同的模态和混合算子。我们跟踪边界的可判定性，并给出了精确的复杂性，大多数片段，特别是包括否定的所有片段。对于单调片段，我们能够区分容易的情况下，从困难的情况下，这取决于允许的一组操作。
2009-06-08 cs.CC cs.LO
Enumeration Complexity of Poor Man's Propositional Dependence Logic
依赖逻辑（英语：Dependence logics）是一个现代的独立和依赖逻辑家族，模仿数据库理论的概念。本文旨在开创依赖逻辑领域中枚举复杂性的研究，从而对数据库查询答案的枚举问题提出一个新的观点。因此，作为第一步，我们调查的问题，枚举所有满足队的公式从一个给定的片段命题依赖逻辑。我们区分由任意函数限制团队规模和参数化版本，其中参数是团队规模。我们表明，多项式延迟可以达到多项式，否则在参数化设置，我们达到FPT延迟。然而，构造的具有多项式延迟的枚举算法需要指数空间。我们证明了一个增量多项式延迟算法存在，它只使用多项式空间。相反，我们表明，对于一般的问题，没有限制的团队规模，在多项式空间中运行的枚举算法不存在。
2018-03-12 cs.CC cs.LO
The complexity of admissible rules of Łukasiewicz logic
研究了无穷值命题逻辑中推理规则的可容许性的计算复杂性。在[13]中，证明了在PSPACE中可检验的是在PSPACE中的可容许性。我们确定这个结果是最优的，即，可容许规则是PSPACE完备的。与此相反，可导出的规则是coNP-完全的。
2012-02-28 cs.CC cs.LO math.LO
Complexity of Existential Positive First-Order Logic
让gamma是一个（不一定是有限的）具有有限关系签名的结构。我们证明了在确定性多项式时间多-一约简下，判定一个给定的存在肯定句是否在Gamma中成立是在对数空间中的或对于CSP（Gamma）_NP类是完全的。在这里，CSP（gamma）_NP是一类问题，可以减少到约束满足问题的伽玛下的非确定性多项式时间多-一减少。
2011-01-12 cs.CC cs.LO
Complexity Results for Modal Dependence Logic
模态依赖逻辑最近由Väänänen引入。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n，=（p_1，...，p_（n-1）;p_n）直观地说明p_n的值由p_1，.，p_（n-1）。Sevenster（J. Logic and Computation，2009）表明，对于非确定性指数时间，模态依赖逻辑的可满足性是完全的。在本文中，我们考虑片段的模态依赖逻辑得到的限制允许命题连接词的集合。我们证明了穷人依赖逻辑的可满足性，这种语言由使用合取、必要性和可能性（即，不允许分离），保持NEXPTIME-完全。如果我们只允许单调公式（没有否定，但有析取），复杂性下降到PSPACE完全性。我们还扩展了Väänänen的语言，允许经典的析取除了依赖析取，并表明可满足性问题仍然是NEXPTIME完全的。如果我们不允许否定和依赖析取，那么对于多项式层次的第二层来说，可满足性是完全的。通过这种方式，我们对Väänänen和Sevenster考虑的命题和依赖运算符的所有限制的可满足性问题的计算复杂性进行了完全分类。
2011-04-04 cs.CC cs.LO
On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic
二阶布尔逻辑是QBF的推广，其常数交替片段已知对于指数时间层次的水平是完全的。我们考虑这种逻辑的两种类型的限制：1）对项构造的限制，2）对布尔矩阵的形式的限制。对于第一类，我们考虑两种限制：首先，不允许嵌套使用适当的函数变量，其次规定每个函数变量必须以固定的参数序列出现。第二种，我们考虑霍恩，克罗姆，和核心片段的布尔矩阵。我们分类的复杂性的逻辑得到这两种类型的限制相结合。我们表明，在大多数情况下，逻辑与k交替块的函数量词是完整的指数时间层次的第k或（k-1）级。此外，我们建立NL-完全的克罗姆和核心片段，当k=1和第一类的限制都有效。
2020-07-08 cs.CC cs.LO
On the freeze quantifier in Constraint LTL: decidability and complexity
约束LTL是LTL在Presburger约束上的推广，通常被用作一种形式语言来描述具有约束的操作模型的行为。冻结量词可以是语言的一部分，如在一些实时逻辑中，但这种变量绑定机制在许多逻辑语言中（一阶时态逻辑，混合逻辑，序列图逻辑，导航逻辑，具有抽象的逻辑等）是相当普遍和普遍的。我们表明，约束LTL在简单的域（N，=）增加了冻结量词是不可判定的，这是一个令人惊讶的结果，鉴于穷人的语言约束（只有平等测试）。许多版本的无冻结约束LTL在具有定性谓词的域上是可判定的，我们的不可判定性结果实际上建立了Sigma_1^1-完备性。在积极的一面，我们提供的复杂性结果时，域是有限的（EXPSPACE-完备性）或当公式是平坦的，在某种意义上介绍的文件。我们的不可判定性的结果是尖锐的（即限制变量的数量），我们所有的复杂性特征确保完整性方面的一些复杂性类（主要是PSPACE和EXPSPACE）。
2006-09-29 cs.CC cs.LO
Complexity of Nonassociative Lambek Calculus with classical logic
本文证明将经典逻辑与非结合兰贝克演算合并得到的BFNL，其后承关系仍可在指数时间内判定，解决了加入经典联结词后保持可判定性的复杂度问题。
2024-12-31 cs.CC cs.LO
The Complexity of Counting Models of Linear-time Temporal Logic
我们确定的复杂性计数模型的有界大小的规格表示的线性时间时序逻辑。如果边界是以一元形式给出的，那么计算单词模型是P-完全的;如果边界是以二进制形式给出的，那么计算非确定性多项式空间图灵机的运行次数是一样困难的。如果边界是以一元形式给出的，那么对树模型进行计数就像对非确定性指数时间图灵机的接受运行进行计数一样困难。对于边界的二进制编码，这个问题至少和计算非确定性指数空间图灵机的接受次数一样困难。另一方面，它并不比计数非确定性双指数时间图灵机的接受运行更难。
2014-10-06 cs.CC cs.LO
Descriptive complexity for pictures languages (extended abstract)
本文用存在二阶逻辑的句法片断来研究任意维图像语言的描述复杂性。- 本文将Giammarresi等人的\cite{GRST96}对存在一元二阶逻辑中的\emph{recognizable}图像语言类的刻画统一推广到任意维。- 我们陈述了在线性时间内识别的图像语言类在任意维的非确定性细胞自动机上的几个逻辑刻画。它们是第一个与机器无关的元胞自动机复杂性类的刻画。我们的刻画基本上是从归一化结果推导出来的，我们证明了一阶和存在的二阶逻辑图片。它们是在一个通用和统一的框架中获得的，该框架允许将它们扩展到其他“常规”结构。最后，我们描述了一些层次结构的结果，表明我们的逻辑刻画的最优性，并划定其限制。
2012-01-27 cs.CC cs.LO
On the decidability and complexity of Metric Temporal Logic over finite words
度量时态逻辑（Metric Temporal Logic，MTL）是一种重要的实时系统规格说明形式。本文证明了有限时间词上MTL的可满足性问题是可判定的，具有非本原递归复杂性。我们还考虑了MTL的模型检查问题：是否所有的话接受一个给定的Alur-Dill时间自动机满足给定的MTL公式。我们证明了这个问题是可判定的有限字。在无限的话，我们表明，模型检验的安全片段的MTL-其中包括不变性和时间有界的响应特性-也是可判定的。这些结果是相当令人惊讶的，因为它们与文献中出现的各种相反的说法相矛盾。
2007-02-28 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
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
Data Complexity in Expressive Description Logics With Path Expressions
TU Dresden（德累斯顿工业大学）；University of Wrocław（弗罗茨瓦夫大学）
本文分析 ZOIQ 在拟森林上可满足性的数据复杂性，证明其 NP 完全，并据此重新刻画 OWL2 SR 族及 ZIQ 根查询蕴涵的复杂性界限。
2024-06-11 cs.AI cs.CC cs.LO
Complexities of Well-Quasi-Ordered Substructural Logics
本文利用序数索引快速增长复杂性类，对具有良拟序的子结构逻辑的可演绎性和可证明性问题进行全面分类，揭示了逻辑设计变化对算法行为的影响。
2025-04-30 cs.CC cs.LO math.LO
Complexity of ITL model checking: some well-behaved fragments of the interval logic HS
模型检验已成功地应用于许多计算机科学领域，包括人工智能、理论计算机科学和数据库。大多数提出的解决方案利用经典的，基于点的时序逻辑，而很少的工作已经做了区间时序逻辑设置。最近，人们提出了有限Kripke结构上Halpern和Shoham的时间区间HS模态逻辑的非初等模型检验算法（在齐性假设下）和它的两个有意义片段的EXPSPACE模型检验过程.在本文中，我们表明，更有效的模型检验程序可以开发一些表达足够的片段HS。
2016-01-13 cs.CC cs.DS cs.LO
Complexity of Non-Monotonic Logics
Leibniz Universität Hannover（汉诺威莱布尼茨大学）
在过去的几十年中，非单调推理已经发展成为计算逻辑和人工智能领域的重要研究课题之一。已经考虑了将非单调方面引入经典逻辑的不同方式，例如，具有缺省规则的扩展、具有模态置信算子的扩展或语义的修改。在这个调查中，我们认为从上述每一种可能性的逻辑形式主义，即赖特的默认逻辑，摩尔的自我认知逻辑和麦卡锡的界限。此外，我们考虑溯因，其中一个是不感兴趣的推理，从一个给定的知识库，但在计算可能的解释观察相对于一个给定的知识库。这些逻辑的命题变体的不同推理任务的复杂性结果已经在90年代进行了研究。然而，近年来，可以观察到对复杂性问题的新的兴趣。一个当前的焦点方法是考虑参数化的问题，并确定合理的参数，允许FPT算法。在另一种方法中，重点在于识别片段，即，限制的逻辑语言，允许更有效的算法，最重要的推理任务。在本调查中，我们重点关注第二个方面。我们描述了通过限制允许的运算符集（例如，禁止否定，可以只考虑单调公式）或只考虑合取范式但具有广义子句类型的公式。我们考虑的算法问题是每个逻辑中的可满足性和蕴涵的合适变体，但也是计数问题，其中人们不仅对某些对象的存在感兴趣（例如，一个公式的模型），但要求他们的号码。
2010-09-10 cs.AI cs.CC cs.LO
On the Complexity of Learning Description Logic Ontologies
University of Bergen（卑尔根大学）
本体是表示领域知识，特别是与生命科学相关的领域中的知识的流行方式。构建本体的过程（半）自动化吸引了来自不同社区的研究人员进入一个称为“本体学习”的领域。我们提供了一个正式规范的准确和可能近似正确的学习模型从计算学习理论。然后，我们从文献中回顾了在这些模型中学习轻量级描述逻辑（DL）本体的复杂性结果。最后，我们强调其他方法在文献中提出的学习DL本体。
2021-03-25 cs.AI cs.CC cs.LG
Lower Bounds for the Complexity of Monadic Second-Order Logic
Courcelle在1990年提出的著名定理指出，在一元二阶逻辑（MSO）中可定义的图的任何性质都可以在线性时间内在任何一类有界树宽的图上确定，或者换句话说，MSO在线性时间内在任何此类图上都是固定参数易处理的。从逻辑的角度来看，Courcelle定理为MSO-模型检验的易处理性建立了一个充分条件或上界。而这样的逻辑复杂性的上限已经在文献中得到了极大的关注，几乎没有什么是已知的相应的下限。本文建立了一元二阶逻辑复杂度的一个强下界。特别是，我们表明，如果C是任何一类图，这是封闭的下采取子图，其树宽是不是有界的多对数函数（事实上，$\log^c n$为一些小c足够），然后MSO-模型检验是棘手的C（在一个适当的假设下，从复杂性理论）。
2011-06-23 cs.CC cs.DM cs.DS
A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics
Computing Laboratory（计算实验室）；Oxford University（牛津大学）；School of Computer Science（计算机科学学院）；University of Manchester（曼彻斯特大学）
本文研究了分级模态逻辑在自反性、序列性、对称性、传递性和欧几里得性等不同组合框架类上的可满足性问题，并为其获得了紧致的复杂性界限。
2009-05-19 cs.AI cs.CC cs.LO
Descriptive complexity of real computation and probabilistic independence logic
我们介绍了一种新的变种BSS机称为分离分支BSS机（简称S-BSS），并开发了一个费根型的逻辑特征的语言可判定的非确定性多项式时间的S-BSS机。我们证明了S-BSS机上的NP严格包含在BSS机上的NP中，并且S-BSS机上的每一种NP语言都是R^n的通常拓扑中闭集的可数并。此外，我们建立，在布尔输入NP上的S-BSS机没有真正的常数的特点的复杂性类existsR（一类问题的多项式时间减少到真正的存在理论的reals）的自然片段，因此位于NP和PSPACE之间。最后，我们应用我们的结果来确定概率独立逻辑的数据复杂性。
2020-07-08 cs.CC cs.LO math.LO
Logical complexity of graphs: a survey
本文讨论了一阶逻辑中有限图的可定义性，它具有两个表示顶点邻接和相等的关系符号。图$G$的逻辑深度$D(G)$等于定义$G$直到同构的句子的最小量词深度。逻辑宽度$W(G)$是在这样的句子中出现的变量的最小数目。逻辑长度$L(G)$是最短定义语句的长度。我们调查已知的估计，这些图的参数，并讨论他们的关系到其他主题（如效率的Weisfeiler-Lehman算法在同构测试，随机图的演变，定量特征的零一律，或贡献的弗兰克拉姆齐的研究希尔伯特的Entscheidungsproblem）。此外，我们跟踪一个图的描述性复杂性的行为，因为逻辑变得更加严格（例如，只允许定义有限数量的变量或量词交替）或更可表达（后与计数量词供电）。
2013-04-29 cs.CC cs.LO math.CO
Non-commutative linear logic fragments with sub-context-free complexity
本文提出了Lambek演算片段对REG、LCFL和CFL类的新的描述复杂性刻画，首次将Lambek演算片段与证明复杂性REG和LCFL等同，并基于直接转换与结构归纳展示了最弱变体的CFL复杂性，确立了Cut消解定理在比较形式文法与矢列演算中的效用。
2025-11-04 cs.CC cs.FL cs.LO
