Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics
我们建立了可判定性的无限多公理扩展的交换全Lambek逻辑与削弱FLew（即IMALLW），有一个切自由hyperprinciple证明演算（具体地说：每一个分析结构规则扩展）。最近建立了其收缩对应物FLec的相应扩展的可判定性，但它们的计算复杂性没有得到回答。在本文的第二部分中，我们引入了足够的长度函数的良好拟序和快速增长的复杂性类，以获得复杂性上界的削弱和收缩扩张。这个结果的一个具体实例产生的第一个复杂性界为突出的模糊逻辑MTL（monoidal t-范数为基础的逻辑）提供了一个长期存在的开放问题的答案。
2021-04-20 cs.LO
Decidability of an Expressive Description Logic with Rational Grading
本文考虑了描述逻辑中实现理性分级的句法对象-概念构造子，即部分限制。部分限制能够表达关于后继集合的合理部分的语句，从本质上丰富了DL的表达能力。我们研究了一个扩展的研究DL ALCQIHR+部分限制，并证明了在扩展逻辑的推理仍然是可判定的。证明使用表格技术与指数技术，旨在处理部分限制。
2019-05-24 cs.LO
A syntactic proof of decidability for the logic of bunched implication BI
本文通过证明论方法，给出了bunched implication逻辑BI可判定性的语法证明，提供了可实现的决策程序并界定了逻辑复杂性。
2026-01-03 cs.LO
Eigenvariables, bracketing and the decidability of positive minimal predicate logic
本文通过括号化机制替代特征变量条件，给出正最小谓词逻辑可判定性的新证明，并推广至简单类型论、二阶命题逻辑及系统F正类型居留问题。
2023-05-15 cs.LO
Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
Hyperproperties是系统的属性，涉及不同的执行轨迹，从安全到对称，并发性的一致性模型等许多应用程序，近年来，不同的线性时间逻辑指定异步hyperproperties进行了研究。虽然这些逻辑的模型检验是不可判定的，但是已经识别出有用的可判定片段，例如用于异步安全分析的应用。在本文中，我们解决异步超性质的时序逻辑的表达性和可判定性问题。我们比较了这些逻辑的表达性，以及S1S的扩展S1S[E]与等级别谓词，通过获得几乎完整的表达性图片。我们还研究了这些逻辑的表达能力时，解释单例集的痕迹。我们表明，对于HyperLTL的两个异步扩展，检查单例模型的存在性已经是不可判定的，对于其中之一，即上下文HyperLTL（HyperLTL_C），我们建立了一个表征的单例模型的扩展标准FO[<]的痕迹与添加。这最后一个结果推广了FO[<]和LTL之间众所周知的等价性。最后，我们确定了新的界限的可判定性的模型检验HyperLTL_C。
2022-07-06 cs.LO
Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus
我们的论文有两个目的：本文首先在Chlebowski和Leszczynska-Jasion的论文“An Investigation into Intuitionistic Logic with Identity”中提出的演算的基础上，给出了一个直觉主义非Fregean逻辑ISCI的演算（Bulletin of the Section of Logic 48（4），p. 259-283，2019），其次，我们通过所获得的系统讨论ISCI的可判定性问题。上述论文中的原始演算没有为ISCI提供可判定性结果。为了得到这个结果，有两个问题需要解决：直觉逻辑的所谓循环特性和由于身份专用规则的形式而缺乏子公式性质。我们讨论可能的路线，以克服这些问题：我们考虑一个较弱的版本的子公式属性，守卫的复杂性公式，可以包括在它里面，我们还提出了一个证明搜索过程，当它失败时，然后存在一个反模型（在Kripke语义ISCI）。
2022-04-14 cs.LO
On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
度量时态逻辑$\mtlfull$是研究最多的实时逻辑之一。它表现出相当大的多样性的表达性和可判定性的基础上允许的一套模式和时间间隔的限制$I$的性质。\oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time.}在本文中，我们通过证明$\mtlsns$（其中$NS$表示非奇异区间）的可满足性在有限逐点严格单调时间上也是可判定的，从而加强了可判定性结果。我们利用时间投影技术给出了从Ouaknine和Worrell的逻辑$\mtls…
2013-11-27 cs.LO
Decidability of the Clark's Completion Semantics for Monadic Programs and Queries
对于一般的逻辑程序（即在子句主体中使用否定的程序），有许多不同的语义。这些语义中的大多数是图灵完备的（在某种意义上可以精确化），这意味着它们是不可判定的。为了获得可判定性，需要对程序和查询施加额外的限制。在逻辑编程中，对底层的一阶语言施加限制是很自然的。在本说明中，我们展示了一元一般程序和查询的克拉克完成语义的可判定性。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-10-23 cs.LO
Decidability of Quantum Modal Logic
Department of Information Engineering, Oita College（大分学院信息工程系）；National Institute of Technology（国立技术研究所）；Oita College（大分学院）
本文利用Harrop引理证明了量子模态逻辑的可判定性，探讨了逻辑系统中判定公式为定理的算法存在性。
2026-03-19 cs.LO math.LO
Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property
Tel Aviv University（特拉维夫大学）
本文通过符号模型性质证明了扩展分层公式的若干片段的可判定性，允许一种类型有自环函数以放宽量词交替约束。
2026-05-13 cs.LO
On Decidability of Expressive Description Logics with Composition of Roles in Number Restrictions
描述逻辑是一种知识表示的形式化方法，在广泛的应用领域中得到了广泛的应用。由于其吸引人的表现力，我们认为在本文中扩展的著名的概念语言ALC允许复杂的角色表达式的数量限制。这些语言首先由Baader和Sattler作为ALCN（M）语言引入，采用了{o，-，And，Or}的角色构造函数M子集。特别是，他们在1999年证明，虽然ALCN（o）是可判定的，但添加其他算子可能很容易导致不可判定性：事实上，ALCN（o，And）和ALCN（o，-，Or）被证明是不可判定的。在这项工作中，我们进一步研究的计算性能的ALCN家庭，旨在缩小可判定性的差距留下开放的Baader和Sattler的结果。特别是，我们将证明ALCN（o）扩展与逆角色在数量和价值的限制变得不可判定，而它可以安全地扩展与合格的数量限制，而不会失去可判定性。
2003-08-19 cs.LO
Classical propositional logic and decidability of variables in intuitionistic propositional logic
我们改进了这个问题的答案：当一个公式中的命题变元在经典命题逻辑中是可证明的时候，在直觉主义命题逻辑中，什么样的被排除的中间集足以证明这个公式。
2014-08-06 cs.LO math.LO
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
研究了带未解释一元谓词的差分逻辑的可判定性，证明实数上带单个未解释一元谓词的量化差分逻辑不可判定，而整数差分逻辑结合实数序与未解释一元谓词仍可判定。
2023-05-24 cs.LO
Decidability results for ATL* with imperfect information and perfect recall
交替时间时序逻辑（ATL*）是多智能体系统的核心逻辑。它的扩展到不完美的信息设置（ATL*i）是众所周知的，有一个不可判定的模型检查问题时，代理有完美的回忆。因此，研究主要集中在没有记忆的代理，或替代语义检索决策。在这项工作中，我们建立了新的决策结果与完美的回忆代理：我们首先证明了一个元定理，允许转移的决策结果类的多人游戏与不完美的信息，如游戏与层次观察，ATL*i的模型检查问题。然后，我们建立了模型检验ATL* 的战略背景和不完善的信息是可判定的限制时，层次实例。
2018-09-03 cs.LO
Residuated Basic Logic II. Interpolation, Decidability and Embedding
证明了剩余基本逻辑$\mathsf{RBL}$的逻辑演算$\mathsf{L_{RBL}}$具有强有限模型性质，并证明了直觉主义逻辑可以嵌入到基本命题逻辑$\mathsf{BPL}$中.因此，$\mathsf{RBL}$是可判定的。证明了剩余基本代数类具有有限可嵌入性，$\mathsf{BPL}$是PSPACE完备的，直觉主义逻辑可以嵌入模态逻辑$\mathsf{K4}$ .
2014-02-24 cs.LO math.LO
Decidability in the logic of subsequences and supersequences
我们考虑一阶逻辑的序列排序的子序列排序，又名序列嵌入。我们证明了B_2理论是不可判定的，回答了Kuske留下的一个问题。关于片段与有限数量的变量，我们表明，FO2理论是可判定的，而FO3理论是不可判定的。
2015-10-14 cs.FL cs.LO
Dynamic Probability Logic: Decidability & Computability
本文针对动态概率逻辑（DPL）的可判定性与可计算性展开研究，构建了弱完备且具有限模型性质（可判定）的证明系统$\u001b[1mH\u001b[0m_{DPL}$，还提出强完备证明系统HDPL并证明其典范模型为可计算结构。
2024-06-24 cs.LO math.LO
Linear Intransitive Temporal Logic of Knowledge LTK_r, Decision Algorithms, Inference Rules
本文研究了具有自反不传递时间关系的知识与时间线性逻辑LTK_r。逻辑在语义上被定义为在具有不传递和自反时间二元关系的特殊框架下为真的公式集合。LTK_r -框架是由自反不传递关系$R_T$连接的簇的线性链.簇内的元素通过模仿不同代理的知识的几个等价关系连接。我们研究公式和推理规则的可判定性问题。公式的可判定性来自可判定性w.r.t.为了研究推理规则的可容许性，我们引入了一些特殊的构造性Kripke模型，用于描述推理规则的可容许性。利用一种特殊的赋值可定义技术，我们找到了一个确定LTK_r中可容许推理规则的算法。也就是说，我们证明了逻辑LTK_r是可判定的，且关于推理规则的可容许性是可判定的。
2014-07-26 cs.LO
Dynamic Epistemic Logic with Communication Actions
这项工作提出了一个动态认知逻辑与通信动作，可以同时进行。与Ditmarsch、Hoek和Kooi提出的并发认知动作逻辑不同，这里的并发机制是所谓的真正并发，这里我们使用的是基于进程演算的方法，如CCS和CSP，以及动作模型逻辑。我们的方法使得证明的可靠性，完整性和可判定性，不同于其他的方法。我们提出了一个公理化，并表明，证明的合理性，完整性和可判定性，可以使用减少的方法。
2019-02-04 cs.LO
Linear Non-Transitive Temporal Logic, Knowledge Operations, Algorithms for Admissibility
本文研究了非传递时态线性逻辑LTL（Past，m）中推理规则的可满足性、可判定性和可容许性、知识概念和主体知识等问题。我们发现算法解决上述问题，证明我们的方法考虑线性非传递时间与几个例子。主要的、最复杂的、技术上的新结果是LTL（Past，m）w.r.t.可接受的规则我们讨论了几种方法来形式化的知识和代理的知识在给定的方法在非传递线性逻辑模型指向过去的概念。
2014-06-11 cs.LO
The Fertile Steppe: Computability Logic and the decidability of one of its fragments
本文系统介绍可计算性逻辑（CoL）及其核心语义、语法和 Cirquent Calculus 证明系统，并针对其公理化系统 CL15 给出可判定性的尝试性证明，同时探讨其在算术与人工智能中的应用价值。
2025-03-05 cs.LO
Trees over Infinite Structures and Path Logics with Synchronization
我们提供了无限树结构的模型检测问题的可判定性和不可判定性的结果。这些树结构由无限关系结构的元素序列构建。更准确地说，我们处理的关系结构M的树迭代在Shelah-Stupp的意义。与经典的MSO逻辑模型检验可判定的结果相反，我们证明了只允许路径量词和链量词的逻辑树模型检验问题的可判定性（其中链是路径的子集），因为它们出现在分支时间逻辑中;然而，同时树被等层关系丰富（如果顶点u、v在相同的树层上，则在顶点u、v之间保持）。我们将树逻辑与用于表达底层结构M的属性的逻辑干净地分离。我们说明的范围内的可判定性的结果表明，两个轻微的扩展框架导致不可判定性。特别地，这适用于Muchnik-Walukiewicz意义上的（更强的）树迭代。
2011-11-14 cs.LO
Decidability of Quasi-Dense Modal Logics
针对带模态归约原理的模态逻辑K扩展的长期可判定性难题，本文提出基于析取存在规则的新型证明系统，证明了准稠密逻辑子类的可判定性，并给出了EXPSPACE判定程序。
2024-06-05 cs.LO math.LO
Decidability of MSO Reparameterization over Countable Chains
Tel Aviv University（特拉维夫大学）
本文研究了如何通过降低表示维度来简化MSO多维点解释，证明在可数标记线性序类上，给定的MSO公式是否允许d维重参数化是可判定的。
2026-05-19 cs.LO
An Application of the Feferman-Vaught Theorem to Automata and Logics for<br> Words over an Infinite Alphabet
我们表明，一个特殊的情况下，Feferman-Vaught组合定理产生了一个自然的概念，自动机的有限字在一个无限的字母表，具有良好的封闭性和可判定性，以及一些逻辑刻画。我们还考虑了一个轻微的扩展的Feferman-Vaught形式主义，它允许表达更多的组件值之间的关系（如平等），并证明相关的可判定性结果。从这个结果，我们得到了新的类的可判定逻辑的词在一个无限的字母表。
2008-03-25 cs.LO
Self-extensional logics of formal inconsistency: Decidability and limits for paraconsistency
Centre for Logic, Epistemology and the History of Science (CLE), University of Campinas (UNICAMP)（坎皮纳斯大学逻辑、认识论与科学史中心）；Institute of Philosophy and the Humanities (IFCH), University of Campinas (UNICAMP)（坎皮纳斯大学哲学与人文学院）
本文研究自扩展次协调逻辑RmbC的可判定性，分类一致性公理，识别爆炸性核心，证明其有限模型性质与可判定性，确定有效性问题的2-EXPTIME上界和coNP困难下界。
2026-09-21 cs.LO
Decidability of modal logics of non-$k$-colorable graphs
本文研究双模态语言下非$k$-可着色图模态逻辑的可判定性，证明非$k$-可着色图（有向或无向）及其部分扩展的模态逻辑是可判定的。
2023-08-04 cs.LO math.LO
Fusions of One-Variable First-Order Modal Logics
Birkbeck, University of London（伦敦大学伯贝克学院）；University of the Witwatersrand（威特沃特斯兰德大学）；University of Liverpool（利物浦大学）
研究单变量一阶模态逻辑独立融合的保持性，证明无等式时克里普克完全性和可判定性在全局与局部后承下保持，有等式时则不保持，并给出共享S5模态的充分条件。
2026-07-01 cs.LO
Decidability of predicate logics with team semantics
我们研究了基于团队语义的谓词逻辑的复杂性。证明了二元独立逻辑和二元包含逻辑的可满足性问题都是NEXPTIME-完全的。此外，我们表明，两个变量的依赖逻辑的有效性问题是不可判定的，从而解决了一个开放的问题，从团队语义文献。我们还简要地分析了依赖逻辑的Bernays-Schönfinkel-Ramsey前缀类的复杂性。
2016-06-18 cs.CC cs.LO math.LO
String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS (Full Version)
我们研究了以连接和有限状态转换器作为原子操作的弦逻辑的可满足性的判定性的基本问题。虽然限制到一种类型的操作产生的可判定性，很少有人知道他们的组合理论，这是特别相关的动态网页在一个更现实的浏览器模型的安全漏洞分析时的可判定性。一方面，单词方程（带有连接的字符串逻辑）不能精确地捕获清理功能（例如htmlescape）和隐式浏览器转换（例如innerHTML突变）。另一方面，转换器遭受能够对消毒功能和浏览器转换建模，但不能对字符串连接建模的相反问题。简单地将词方程和转换器组合在一起很容易导致不可判定的逻辑。我们的主要贡献是表明，“直线片段”的逻辑是可判定的（复杂性范围从PSPACE到EXPSPACE）。该片段可以表达的程序逻辑的直线字符串操作程序的连接和转换作为原子操作，这出现在执行有界模型检验或动态符号执行。我们证明了逻辑可以自然地表达分析Web应用程序中的突变XSS所需的约束。最后，在存在长度、字母计数、正则、indexOf和不等性约束的情况下，逻辑仍然是可判定的。
2015-11-05 cs.LO
A separation logic for sequences in pointer programs and its decidability
Peking University（北京大学）；Guangzhou University（广州大学）；Zhengzhou University（郑州大学）
分离逻辑及其变体可以描述指针程序的各种属性。然而，当涉及到序列的属性时，人们可能会发现很难形式化。为了处理变长序列和多级数据结构的属性，我们提出了序列堆分离逻辑，它将序列集成到堆操作程序的逻辑推理中。序列变量上的量词和存储序列的单例堆（序列单例堆）是我们逻辑中的新成员。进一步，我们研究了两个片段的可满足性问题。序列-堆分离逻辑的命题片断是可判定的，程序变量有2个交替、序列变量有1个交替的片断是不可判定的。此外，我们探索与前趋范式的逻辑的可判定和不可判定的片段之间的边界。
2023-01-16 cs.CL cs.LO
Possibilistic Computation Tree Logic over Finitely-Valued Kripke Structures: Decidability and Complete Axiomatization
Shaanxi Normal University（陕西师范大学）
本研究针对尚未探讨的PoCTL可满足性问题，通过相关技术证明其可在指数时间内判定，并给出该逻辑的完备公理化，完善了PoCTL的理论基础。
2026-09-22 cs.LO
Logics for Epistemic Actions: Completeness, Decidability, Expressivity
我们考虑动态版本的认知逻辑，如Baltag和Moss的“认知程序的逻辑”（2004）中所阐述的。这篇论文提出了一种动态认知逻辑的逻辑语言（实际上是由动作签名参数化的语言家族）。已有研究表明，该语言的有效性是Pi-1-1-完备的，因此不存在递归公理化的完备逻辑系统，而本文则证明了无动作迭代的片段的弱完备性结果，以及无动作迭代的片段和常识的强完备性结果。我们的工作涉及到术语重写理论的迂回。该论点使用模态过滤，因此我们得到有限的模型属性，因此可判定性。我们也给我们最大的语言翻译成PDL，从而获得第二个证明的可判定性。本文最后给出了一些关于表达能力的结果。这些主要涉及比较动作迭代自由语言与模态逻辑增强传递闭包运算符。我们回答了一个自然的问题，我们通过不同的动作签名获得的语言：我们证明了一个逻辑语言与运营商的私人公告更有表现力比一个公共公告。
2022-03-13 cs.LO math.LO
Strategy Logic with Imperfect Information
我们介绍了一个扩展的策略逻辑的信息设置，称为SLii，并研究其模型检测问题。由于这种逻辑很自然地捕捉到了具有不完美信息的多人博弈，因此问题是不可判定的。我们引入了一个语法类的“层次实例”，直观地说，作为一个去语法树的公式，战略量化关注的模型的更精细的观察。我们证明了模型检查SLii限制到层次实例是可判定的。这一结果，因为它允许复杂的模式存在和普遍量化的战略，大大概括了以前的，如决策的多人游戏与不完美的信息和分层的意见，决策的分布式综合分层系统。为了建立可判定性结果，我们引入并研究QCTL * ii，QCTL * 的扩展（本身是CTL * 的扩展，具有二阶量化的原子命题），通过用观测值参数化其量词。QCTL * ii的简单语法使我们能够在概念上将SLii简化为QCTL * ii，从而将关注点分开，允许人们忘记策略和参与者，只关注二阶量化。虽然QCTL * II的模型检查问题是，在一般情况下，不可判定的，我们确定的语法片段的分层公式和证明，使用自动机理论的方法，它是可判定的。SLii的可判定性结果如下，因为约简将SLii的分层实例映射到QCTL * ii的分层公式。
2018-09-03 cs.LO
The Tree Width of Separation Logic with Recursive Definitions
分离逻辑是一种广泛使用的形式主义，用于描述动态分配的链接数据结构，如列表，树等的逻辑的各个片段的可判定性状态构成了一个长期存在的开放问题。目前的结果报告的技术，以确定满足性和有效性的蕴涵分离逻辑（S）的列表（可能与数据）。在本文中，我们建立了一个更一般的可判定性结果。我们证明了任何使用较一般的递归定义谓词的分离逻辑公式都是可判定的可满足性，而且这些公式之间的蕴涵也是可判定的有效性.这些谓词足够通用，可以定义（双）链表、树和比树更通用的结构，比如叶子被链接在一个链表中的树。可判定性证明是通过将一元二阶逻辑在有界树宽度的图上的可判定性归约来实现的。
2013-03-30 cs.FL cs.LO
Logical Queries over Views: Decidability and Expressiveness
我们研究的问题，决定可满足性的一阶逻辑查询的意见，我们的目的是划定边界之间的可判定和不可判定的片段，这种语言。由于视图在信息集成和数据仓库等应用中的作用，视图目前在数据库研究中占据中心地位。我们的主要结果是确定一个可判定类的一阶查询一元合取的意见，概括了经典类的一阶句子一元关系，称为Lowenheim类的可判定性。然后，我们演示了如何这个类的各种扩展导致不可判定性，也提供了一些表现力的结果。除了它的理论兴趣，我们的新的可判定类是潜在的有趣的应用，如决定复杂的依赖关系的含义，分析一类受限制的主动数据库规则，本体推理。
2008-03-18 cs.DB cs.LO
Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering
我们考虑一阶逻辑的子字排序有限的话，每个字是作为一个常数。我们的第一个结果是，$Σ_1$理论是不可判定的（已经超过两个字母）。我们调查的可判定性边界考虑片段，但一定数量的变量交替有界，这意味着变量必须始终量化的语言与有限数量的字母交替。我们证明了当至多两个变量不是交替有界的，$Σ_1$片段是可判定的，当三个变量不是交替有界的，它变得不可判定。对于更高的量词交替深度，我们证明了$Σ_2$片段已经是不可判定的一个变量没有交替界，当所有的变量是交替有界的，整个一阶理论是可判定的。
2021-09-24 cs.FL cs.LO
The Topological Mu-Calculus: completeness and decidability
我们研究了拓扑$μ$ -演算，基于Cantor导数和闭包模态，证明了在一般拓扑空间上，以及在$T_0$和$T_D$空间上的完备性、可判定性和FMP.我们还调查关系$μ$ -演算，提供一般完整性结果的所有自然片段的$μ$ -演算在许多不同类别的关系框架。与大多数其他这样的证明$μ$演算，我们是模型理论，使一个创新的使用已知的模态逻辑方法（-“最终”子模型的规范模型），具有极大的一般性和本质上的简单性的双重优势。
2021-05-18 cs.LO
HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories
我们提出了一个简单的决议证明系统高阶约束霍恩条款（HoCHC）-系统的高阶逻辑模理论-并证明其可靠性和反驳的完整性w.r.t.标准语义。作为推论，我们得到了HoCHC的紧性定理和半可判定性的背景理论，我们证明了HoCHC满足一个典型的模型性质。此外，从高阶到1阶逻辑的著名的翻译的一个变体被证明是健全的和完整的HoCHC在标准语义。我们说明了如何转移的可判定性结果（片段）一阶逻辑模理论，我们的高阶设置，作为例子的Bernays-Schonfinkel-Ramsey片段HoCHC模的限制形式的线性代数算术。
2019-04-19 cs.LO
A Survey on Temporal Logics
本文综述了广义时态逻辑的主要研究和最新研究，介绍了各种时态逻辑系统，处理了各种时态结构，讨论了时态逻辑的重要特征，如可判定性（或不可判定性）结果、可表达性和证明系统。
2011-04-25 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
Decidability and Undecidability Results for Propositional Schemata
CNRS（法国国家科学研究中心）
我们定义了一个逻辑的命题公式图式添加到语法的命题逻辑索引命题和迭代连接词范围内的算术变量参数化的区间。可满足性问题是不可判定的，这个新的逻辑，但我们引入了一个非常一般的类的模式，称为有界线性，这个问题变得可判定。这个结果是通过减少到一个特定的类称为定期的模式，我们提供了一个健全的和完整的终止证明过程。这种模式演算允许一个捕获证明模式对应于一个大类的命题逻辑中指定的问题。我们还表明，可满足性问题再次成为不可判定的轻微扩展这一类，从而表明，有界线性模式代表了一个很好的妥协之间的表达性和可判定性。
2014-01-16 cs.AI cs.LO
Making Metric Temporal Logic Rational
本文研究了$\mtl$在点时间上的一个扩张，它具有有理表达式保护模态$\reg_I(\re)$，其中$\re$是子公式上的有理表达式.我们研究了这个扩展（$\mtl$ + $φ\ureg_{I, \re} φ$ + $\reg_{I,\re}φ$），称为$\regmtl$，以及它的片段$\sfmtl$的可判定性和表达性，其中只允许无星有理表达式。利用时间投影技术，我们证明了$\regmtl$具有可判定的可满足性，给出了$\mtl$的一个等价约简。我们还确定了一个子类$\mitl+\ureg$的$\regmtl$，我们的等价满足减少产生的公式$\mitl$，产生基本的可判定性。作为我们的第二个主要结果，我们显示了一个紧密的自动机逻辑之间的连接$\sfmtl$和偏序（或非常弱）1-时钟交替时间自动机。
2017-04-29 cs.LO
Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions
Free University of Bozen-Bolzano（博尔扎诺自由大学）；King's College London（伦敦国王学院）；Birkbeck, University of London（伦敦大学伯贝克学院）；University of Liverpool（利物浦大学）
本文系统研究一阶模态逻辑中非刚性常项、限定摹状词和计数特征对可判定性的影响，证明若干一元片段可判定并给出紧致复杂度界，同时指出一种扩展逻辑的Ackermann困难性。
2026-11-02 cs.LO math.LO
Ticket Entailment is decidable
我们证明了票蕴涵的可判定性。Anderson和Belnap在关联逻辑的框架内提出的这个问题等价于具有部分基BB'IW的简单类型组合逻辑中的类型栖居的可判定性问题。本文解决了单纯型微积分对遗传右极大项的限制的类型栖居等价问题。
2012-07-05 cs.LO
Bundled fragments of first-order modal logic: (un)decidability
Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）
量化模态逻辑为模态态度的推理提供了一种自然的逻辑语言，即使在保留量化的丰富性的同时，也可以引用域上的谓词。但是，在许多模型类上，逻辑的大多数片段都是不可判定的。多年来，只有少数片段（例如单声部）被证明是可判定的。在本文中，我们研究的片段，捆绑量词和模态在一起，知识/为什么/什么的认知逻辑的早期工作的启发。与量化模态逻辑一样，域是否在世界上保持相同会产生重大差异。特别是，我们表明，束$\forall \Box$是不可判定的恒定域的解释，即使只有一元谓词，而$\exists \Box$束是可判定的。另一方面，在增加域解释，我们得到的可判定性与$\forall \Box$和$\exists \Box$束与不受限制的谓词。在这些情况下，我们还获得了在\PSPACE中运行的基于tableau的过程。我们进一步表明，$\exists \Box$束不能区分恒定域和增加域的解释。
2018-03-28 cs.AI cs.LO math.LO
Non-Rigid Designators in Modal and Temporal Free Description Logics (Extended Version)
本研究提出带非严格限定摹状词与名称的模态描述逻辑，关联一阶模态逻辑单变量片段可满足性，证明$\n mathbf{S5}^{n}$等逻辑概念可满足性为NEXPTIME完全，还分析了时态逻辑可判定性。
2024-09-10 cs.LO
On the Decidability of Connectedness Constraints in 2D and 3D Euclidean Spaces
我们调查（无量词）空间约束语言的平等，接触和连通性谓词，以及布尔运算的区域，解释低维欧氏空间。我们表明，推理的复杂性显着变化取决于空间的尺寸和所考虑的区域的类型。例如，具有邻接连通性谓词（且无接触）的逻辑在欧氏平面中的多边形或正则闭集上是不可判定的，在三维欧氏空间中的正则闭集上是NP完全的，在三维欧氏空间中的多面体上是ExpTime完全的。
2011-04-01 cs.LO
Set Automata and Limits of Decidability of Two-Variable Logic on Data Words
Tata Institute of Fundamental Research（塔塔基础研究所）；Indian Institute of Technology Goa（印度理工学院果阿分校）
研究扩展数据词双变量逻辑以包含guarded regular二元谓词，定义了idempotent monoids的决定性条件，并引入set automata形式化，证明其与ordered quasi-normal set automata的等价性。
2026-05-09 cs.FL cs.LO
Metric Temporal Logic with Counting
在资源受限的实时的计算规范中，能够计算在指定时间间隔内事件发生的次数是非常有用的。在本文中，我们研究了度量时态逻辑（$\mathsf{MTL}$）的扩展与两个不同的计数模态称为$\mathsf{C}$和$\mathsf{UT}$（直到与阈值），这提高了表达能力的$\mathsf{MTL}$在正交的方式。我们仅限于有限时间词上逐点解释的$\mathsf{MTL}$的未来片段。我们提供了一个全面的研究的表达能力的逻辑$\mathsf{CTMTL}$和它的片段使用EF游戏扩展与适当的计数移动的技术。最后，作为我们的主要结果，我们建立了$\mathsf{CTMTL}$的可判定性，给出了从$\mathsf{CTMTL}$到$\mathsf{MTL}$的等价约简。这种减少提供了一个使用时间预测的例子，上面介绍了过采样来证明可判定性。我们的约简也意味着用$\mathsf{C}$和$\mathsf{UT}$模态扩展的$\mathsf{MITL}$是基本可判定的。
2015-12-30 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
The logical strength of Büchi's decidability theorem
本文在弱二阶算术理论 RCA_0 中证明了 Büchi 可判定性定理等价于 Σ^0_2 归纳模式、加法着色 Ramsey 定理及 Büchi 补集定理，并蕴含 McNaughton 确定性定理和有界宽度 König 引理。
2019-05-22 cs.LO math.LO
Most Properties are Undecidable for Transitive Tense Logics
The Tsinghua-UvA JRC for Logic Department of Philosophy Tsinghua University（清华大学哲学系清华-阿姆斯特丹逻辑联合研究中心）；Institute for Logic, Language and Computation University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）
本文通过从Minsky机器的不可判定问题归约，证明了传递时态逻辑格NExt(K4t)中大多数性质（如Kripke完全性、有限模型性质和可判定性）是不可判定的。
2026-09-11 cs.LO math.LO
From Interpolating Formulas to Separating Languages and Back Again
King’s College London（伦敦国王学院）；University of Liverpool（利物浦大学）；Birkbeck, University of London（伦敦大学伯贝克学院）
本文探讨了Craig插值的扩展形式，包括在无CIP逻辑中的插值问题，以及形式语言中的分离问题，并展示了这些研究如何相互关联。
2025-12-03 cs.LO
