任意箭头更新逻辑的不可判定性

箭头更新合成

Arrow Update Synthesis

在这方面的贡献，我们提出了任意箭头更新模型逻辑（AAUML）。这是一种动态认知逻辑或更新逻辑。在更新逻辑中，静态/基本模态在给定的关系模型上被解释，而动态/更新模态引起关系模型的转换（更新）。在AAUML中，更新模态形式化了箭头更新模型的执行，并且还有一种用于量化箭头更新模型的模态。箭头更新模型是众所周知的动作模型的替代方案。我们提供了一个公理化的AAUML。公理化是一个重写系统，允许从任何给定的公式中消除箭头更新模态，同时保持真理。因此，AAUML是可判定的，同样表达的基础多代理模态逻辑。我们的主要结果是建立箭头更新合成：如果有一个箭头更新模型，在该模型之后，我们可以从phi构建（合成）该模型。我们还指出了箭头更新逻辑，动作模型逻辑和精化模态逻辑之间的更新表达性的一些怀孕的差异。

模态和描述逻辑的统一和容许问题的不确定性

Undecidability of the unification and admissibility problems for modal and description logics

我们表明，统一问题`是否有一个替代实例的一个给定的公式，是证明在一个给定的逻辑？对于用泛模态扩充的基本模态逻辑K和K_4，因此，推理规则的容许性问题对于这些逻辑也是不可判定的。这些是标准可判定模态逻辑的第一个例子，其中统一和容许问题是不可判定的。我们还证明了不可判定性的统一和容许问题的K和K4至少有两个模态算子和名（而不是通用模态），从而表明这些问题是不可判定的基本混合逻辑。最近，统一已被引入作为一个重要的推理服务的描述逻辑。带名项的K的不可判定性证明可以用来证明带名项的布尔描述逻辑（如ALCO和SHIQO）的统一的不可判定性。对于具有泛模态的K的不可判定性证明可以用来表明，对于具有传递角色、反向角色和角色层次（如SHI和SHIQ）的布尔描述逻辑，与角色盒相关的统一问题是不可判定的。

基于Lukasiewicz t-范数GCI的模糊描述逻辑的不可判定性

On the Undecidability of Fuzzy Description Logics with GCIs with Lukasiewicz t-norm

最近有一些意想不到的结果，模糊描述逻辑（FDLs）与一般概念包含（GCI）。他们表明，与经典的情况下，DL ALC与GCI不具有有限的模型属性下Lukasiewicz逻辑或产品逻辑，具体地说，知识库可满足性是一个不可判定的问题产品逻辑。我们在这里完成的分析表明，知识库可满足性也是一个不可判定的问题Lukasiewicz逻辑。

量化公告的不可判定性

The Undecidability of Quantified Announcements

本文证明APAL、GAL和CAL三种量化公告逻辑在多智能体情形下不可判定，单智能体情形下可判定，并修正了此前版本中公式cga(X)的定义错误。

$\mathsf{Cheq}$ 的不可有限公理化与不可判定性

Non-finite Axiomatizability and Undecidability of $\mathsf{Cheq}$

本文证明了逻辑 $\mathsf{Cheq}$ 不可有限公理化，并利用 Medvedev 逻辑的不可判定性推导出 $\mathsf{Cheq}$ 的不可判定性。

Undecidability and non-axiomatizability of modal many-valued logics

In this work we study the decidability of a class of global modal logics arising from Kripke frames evaluated over certain residuated lattices, known in the literature as modal many-valued logics. We exhibit a large family of these modal logics which are undecidable, in contrast with classical modal logic and propositional logics defined over the same classes of algebras. This family includes the global modal logics arising from Kripke frames evaluated over the standard Lukasiewicz and Product algebras. We later refine the previous result, and prove that global modal Lukasiewicz and Product lo…

DLFD有限模型推理的不可判定性

Undecidability of Finite Model Reasoning in DLFD

解决了一个关于路径函数依赖的有限逻辑蕴涵的公开问题。

“大多数”导致不可判定性：向LTL添加频率失败

"Most of" leads to undecidability: Failure of adding frequencies to LTL

有限迹上的线性时态逻辑是形式化验证中常用的一种健壮的规范框架。然而，尽管近年来对逻辑的兴趣很高，但其定量扩展的主题尚未得到充分探讨。这项工作的主要目标是研究添加弱形式的百分比约束（例如，大多数的位置在过去满足给定的条件，或sigma是最频繁的字母发生在过去）的LTL片段的效果。这种扩展可能用于验证影响网络或统计推理。不幸的是，正如我们在论文中证明的那样，事实证明，即使是很小的LTL片段的百分比扩展也具有不可判定的可满足性和模型检查问题。我们的不可判定性证明，不仅锐化了大多数的不可判定性结果的逻辑与算术解释的话从文献中已知的，但也是相当简单的。我们还证明了通过限制否定的允许使用可以避免不可判定性，并简要讨论了不可判定性结果如何转移到一阶词逻辑。

Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter

We prove that the positive fragment of first-order intuitionistic logic in the language with two variables and a single monadic predicate letter, without constants and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals [QBL, QKC] and [QBL, QFL], where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser's basic and formal logics, respectively. We also show that, for most "natural" first-order modal logics, the two-variable …

弱版本 MSO+U 的不可判定性

Undecidability of a weak version of MSO+U

本文证明在 $\omega$-词上扩展二阶谓词 $U_1$ 的 MSO 不可判定，并推论允许量化最终周期集合时 MSO 也不可判定。

命题模式的可判定性和不可判定性结果

Decidability and Undecidability Results for Propositional Schemata

我们定义了一个逻辑的命题公式图式添加到语法的命题逻辑索引命题和迭代连接词范围内的算术变量参数化的区间。可满足性问题是不可判定的，这个新的逻辑，但我们引入了一个非常一般的类的模式，称为有界线性，这个问题变得可判定。这个结果是通过减少到一个特定的类称为定期的模式，我们提供了一个健全的和完整的终止证明过程。这种模式演算允许一个捕获证明模式对应于一个大类的命题逻辑中指定的问题。我们还表明，可满足性问题再次成为不可判定的轻微扩展这一类，从而表明，有界线性模式代表了一个很好的妥协之间的表达性和可判定性。

无限结构上的树与同步路径逻辑

Trees over Infinite Structures and Path Logics with Synchronization

我们提供了无限树结构的模型检测问题的可判定性和不可判定性的结果。这些树结构由无限关系结构的元素序列构建。更准确地说，我们处理的关系结构M的树迭代在Shelah-Stupp的意义。与经典的MSO逻辑模型检验可判定的结果相反，我们证明了只允许路径量词和链量词的逻辑树模型检验问题的可判定性（其中链是路径的子集），因为它们出现在分支时间逻辑中;然而，同时树被等层关系丰富（如果顶点u、v在相同的树层上，则在顶点u、v之间保持）。我们将树逻辑与用于表达底层结构M的属性的逻辑干净地分离。我们说明的范围内的可判定性的结果表明，两个轻微的扩展框架导致不可判定性。特别地，这适用于Muchnik-Walukiewicz意义上的（更强的）树迭代。

命题非结合线性逻辑的判定问题及其推广

Decision Problems for Propositional Non-associative Linear Logic and Extensions

在我们以前的工作中，我们提出了从完全非结合Lambek演算通过添加一种线性逻辑模态获得的逻辑。我们称这种逻辑为非关联非交换直觉线性逻辑（简称$\mathbf{NACILL}$）。在本文中，我们建立了可判定性和不可判定性结果的各种扩展的$\mathbf{NACILL}$。关于可判定性的结果，我们证明了$\mathbf{NACILL}$的几个推广的演绎问题与左弱化规则是可判定的。关于不可判定性结果，我们证明了非结合非交换经典线性逻辑的所有扩张的压缩和交换规则的可证明性问题是不可判定的。

传递框架上混合逻辑的复杂性

Complexity of Hybrid Logics over Transitive Frames

本文研究了传递框架、传递树和线性框架上的混合逻辑的复杂性。我们证明了在传递框架上的可满足性是NEXPTIME-完全的。这与这种语言在任意框架上的可满足性的不可判定性形成对比（Areces，Blackburn，Marx 1999）。它还表明，添加@运营商或过去的模态导致不可判定传递框架。这再次与传递树和线性框架的情况形成对比，在这些情况下，我们证明这些语言是非元素可判定的。此外，我们建立了2 EXPTIME和EXPTIME上界可满足的传递框架和传递树，分别为混合直到/因为语言。一个EXPTIME下限保持模态直到语言在两个框架类。

比较与对照阿罗不可能定理与哥德尔不完备定理

Comparing and Contrasting Arrow's Impossibility Theorem and Gödel's Incompleteness Theorem

本文引入自指涉系统这一一般数学对象，通过抽象对角化与不动点论证，形式化阿罗不可能定理与哥德尔第一不完备定理之间的对应关系，并揭示两者产生不可能性机制的细微差异。

探索具有描述逻辑特征的命题动态逻辑的非正则扩展

Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features

本文研究非正则路径表达式对 ALC 扩展描述逻辑可判定性的影响，证明 ALCvpl 在加入 Self 或 nominals 后概念可满足性不可判定，并确立含非正则原子的查询蕴涵不可判定。

关于传递模态多值逻辑

On Transitive modal many-valued logics

本文主要研究由赋值Kripke框架定义的模态逻辑，特别是在某些剩余格上赋值传递Kripke框架的模态逻辑的可计算性和可表示性问题。它表明，一个大家庭的这些逻辑-包括所产生的标准MV和产品代数-产生一个不可判定的后果关系。随后，传递模态Lukasiewicz逻辑的行为进行了比较，它的非传递对应，展示了一些细节有关的可计算性和等价与其他逻辑。最后，我们展示了不可判定性的有效性和局部SAT问题的传递模型时，Delta操作添加到逻辑。

基于逻辑刻画的图神经网络可判定性

Decidability of Graph Neural Networks via Logical Characterizations

本文利用Presburger量词等可判定逻辑刻画图神经网络的表达能力，建立了精确对应关系，并据此提出了GNN验证问题的判定过程，同时证明了相关静态分析与验证问题的不可判定性。

关于计划存在性问题的不可判定性证明

An Undecidability Proof for the Plan Existence Problem

本文证明在特定条件下，计划存在性问题不可判定，揭示了该问题的复杂性。

Medvedev逻辑是不可判定的

Medvedev logic is undecidable

本文通过将周期性平铺问题归约到非定理性，证明了Medvedev逻辑不可判定，并类似地证明了Skvortsov逻辑的不可判定性及两者的区别，解决了一个长期开放问题。

递归方案、MSO逻辑与U量词

Recursion Schemes, the MSO Logic, and the U quantifier

本文证明了对递归方案生成的树，在MSO逻辑基础上增加受限的U量词（表示对任意大有限集为真）后，模型检验问题仍可判定，且该逻辑具有反射性和有效选择性质。

拓扑关系的模态逻辑

Modal Logics of Topological Relations

空间区域间关系推理的逻辑形式在地理信息系统、空间和约束数据库以及人工智能中的空间推理中起着重要作用。在类比Halpern和Shoham的模态逻辑的时间间隔的基础上的艾伦关系，我们介绍了一个家庭的模态逻辑配备了八个模态运营商，解释的Egenhofer-Franzosa（或RCC 8）的关系区域之间的拓扑空间，如真正的平面。我们调查的表达能力和计算复杂性的逻辑得到这种方式。事实证明，我们的模态逻辑具有与一阶逻辑的双变量片段相同的表达能力，但简洁性呈指数级下降。其复杂性范围从（不可判定和）递归可判定到高度不可判定，其中递归可判定逻辑是通过考虑拓扑空间诱导结构的子结构得到的.由于我们的不可判定性结果也捕获了基于实数线的逻辑，它们改进了Halpern和Shoham的区间时间逻辑的不可判定性结果。我们还分析了基于五个RCC 5关系的模态逻辑，关于表达能力的结果类似，但关于复杂性的结果较弱。

真正模态判断的箭头式不可能性

Arrow-Type Impossibility for Genuinely Modal Judgments

本文研究当聚合对象必须是真正模态判断而非事实命题时，Arrow式不可能性是否仍然存在，并通过语义归约和局部到全局的框架机制证明了在稀疏模态设置下的不可能性定理。

Resource dependent undecidability: computability landscape of distinct Turing theories

Can a problem undecidable with classical resources be decidable with quantum ones? The answer expected is no; as both being Turing theories, they should not solve the Halting problem - a problem unsolvable by any Turing machine. Yet, we provide an affirmative answer to the aforesaid question. We come up with a novel logical structure to formulate infinitely many such problems for any pair of distinct Turing theories, including but not limited to the classical and quantum theories. Importantly, a class of other decision problems, such as the Halting one, remains unsolvable in all those theories…

带守卫片段遇上动态逻辑：正则守卫的故事（扩展版）

Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Version)

本研究提出带正则守卫的守卫片段（RGF），统一推广多种GF扩展，证明其可满足性为2EXPTIME完全，查询蕴含不可判定，并确定最大EXPSPACE完全片段。

实时的模型检验：参数无处不在

Real-Time Model-Checking: Parameters everywhere

本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。

First-order logic with self-reference

We consider an extension of first-order logic with a recursion operator that corresponds to allowing formulas to refer to themselves. We investigate the obtained language under two different systems of semantics, thereby obtaining two closely related but different logics. We provide a natural deduction system that is complete for validities for both of these logics, and we also investigate a range of related basic decision problems. For example, the validity problems of the two-variable fragments of the logics are shown coNexpTime-complete, which is in stark contrast with the high undecidabili…

一元二阶逻辑与自相似图上的多米诺骨牌问题

Monadic second-order logic and the domino problem on self-similar graphs

我们考虑了自相似群的Schreier图上的多米诺骨牌问题，以及更一般的一元二阶逻辑。一方面，我们证明了如果群是有界的，那么图的一元二阶逻辑是可判定的。这包括，例如，Sierpienski垫片图和Schreier图的Basilica集团。另一方面，我们已经证明了一类自相似群的多米诺骨牌问题的不可判定性，回答了Barbieri和Sablik的一个问题，以及一些例子，包括线性增长。

Temporal Stream Logic modulo Theories (Full Version)

Temporal stream logic (TSL) extends LTL with updates and predicates over arbitrary function terms. This allows for specifying data-intensive systems for which LTL is not expressive enough. In the semantics of TSL, functions and predicates are left uninterpreted. In this paper, we extend TSL with first-order theories, enabling us to specify systems using interpreted functions and predicates such as incrementation or equality. We investigate the satisfiability problem of TSL modulo the standard underlying theory of uninterpreted functions as well as with respect to Presburger arithmetic and the …

A quantitative extension of Interval Temporal Logic over infinite words

Model checking for Halpern and Shoham's interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics). Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of the given Kripke structure, assuming in addition homogeneity in the propositional valuation. We introduce a quantitative extension of HS over traces, called Difference HS (DHS) allowing one to express timing constraints on the difference amon…

关于带数据局部一阶逻辑的可满足性

On the Satisfiability of Local First-Order Logics with Data

本文研究带数据一阶逻辑的可满足性问题，提出局部片段限制量化范围，证明半径-1片段可判定而更大半径不可判定，并给出存在片段完整的可判定性与复杂性图景。

具有长度和正则表达式约束的字方程的（Un）可判定性结果

(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints

我们证明了几个可判定性和不可判定性结果的可满足性和有效性问题的语言，可以表示解决方案的字方程的长度约束。这种语言上的原子公式是字符串项上的等式（单词等式）、长度函数上的线性不等式（长度约束）和正则集中的成员资格。这些问题在逻辑、程序分析和形式化验证中很重要。这些问题的变体已经被数学家研究了几十年。最近，这些公式的实际可满足性程序（又名SMT求解器）在字符串操作程序（如Web应用程序）的安全分析中变得越来越重要。我们证明了三个主要定理。首先，我们给出了一个新的证明不可判定的有效性问题的一组句子写为一个forall-exists量词交替应用于正字方程。这个不可判定性结果的一个推论是，这个集合是不可判定的，即使句子中最多出现两次字符串变量。第二，我们考虑布尔组合的量词自由公式构建的词方程和长度约束。我们表明，如果字方程可以转换为一个解决的形式，在实践中相关的形式，然后满足性问题的布尔组合的字方程和长度约束是可判定的。第三，我们证明了无量词公式在正则解形式、长度约束和正则表达式上的成员谓词上的可满足性问题也是可判定的。

为什么命题量词使得树上的模态逻辑和时态逻辑变得稳健困难？

Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

本文研究树语义下带命题量词的模态与时态逻辑的复杂性，证明限制于EX的tQCTL已是Tower困难，并在N有界树上为AExpPol完全，同时推广到多种模态逻辑。

基本模态逻辑中的可满足性与有限可满足性

Satisfiability vs. Finite Satisfiability in Elementary Modal Logics

我们研究基本模态逻辑，即模态逻辑考虑一阶可定义类的框架。模态逻辑的经典语义允许无限结构，但实际应用往往要求我们将注意力限制在有限结构上。初等模态逻辑的许多可判定性和不可判定性结果分别在一般可满足性和有限可满足性下得到了证明[11，12，16，17]。在本文中，我们表明，有一个原因，我们必须分别处理这两种可满足性-我们证明，有一个通用的一阶公式，定义了一个基本模态逻辑与可判定的（整体）可满足性问题，但不可判定的有限可满足性问题，反之亦然，存在一个普适公式，它定义了一个具有可判定的有限可满足性问题但具有不可判定的一般可满足性问题的初等模态逻辑。

Sahlqvist Correspondence Theory for Sabotage Modal Logic

Sabotage modal logic (SML) is a kind of dynamic logics. It extends static modal logic with a dynamic modality which is interpreted as "after deleting an arrow in the frame, the formula is true". In the present paper, we are aiming at solving an open problem, namely giving a Sahlqvist-type correspondence theorem for sabotage modal logic. In this paper, we define sabotage Sahlqvist formulas and give an algorithm to compute the first-order correspondents of sabotage Sahlqvist formulas. We give some remarks and future directions at the end of the paper.

Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity

We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking re…

技术报告：资源约束的ATL模型检验及资源的生产和消耗

Technical Report: Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources

文献中已经提出并研究了几种表示资源约束下联盟能力的逻辑。已有的工作表明，如果只考虑资源的消耗，或者系统中任意路径上产生或消耗的资源总量是有界的，那么几种标准逻辑（如资源有界联合逻辑（RB-CL）和资源有界交替时序逻辑（RB-ATL））的模型检验问题是可判定的.然而，对于具有无限资源生产和消费的联盟逻辑，只知道一些不可判定性结果。本文证明了资源无限生产和无限消耗的RB-ATL的模型检验问题是可判定的，但是EXPSPACE困难的.我们还调查了一些易于处理的情况下，并提供了一个详细的比较，资源逻辑RAL的一个变种，连同新的复杂性结果。

补全图景：带逆模态的分级模态逻辑的复杂性

Completing the Picture: Complexity of Graded Modal Logics with Converse

本文填补了带分级逆模态的分级模态逻辑在传统框架类上的复杂性分类空白，证明了其在欧几里得框架上的NExpTime完全性，并证实了其变体在传递框架上的可判定性。

描述逻辑本体的计算Horn重写

Computing Horn Rewritings of Description Logics Ontologies

我们研究的问题重写本体O1表示在DL L1到本体O2在霍恩DL L2，使O1和O2是equisatifiable扩展时，与任意数据集。允许这种重写的本体服从于推理技术，以确保数据复杂性的易处理性。在L1扩展ALCF时显示不可判定性后，我们专注于设计有效的可检查条件，以确保霍恩重写的存在。通过提升现有的技术，将析取数据重写成普通数据的情况下，任意一阶程序与功能符号，我们确定了一类本体，承认霍恩重写多项式的大小。我们的实验表明，许多现实世界的本体满足我们的充分条件，从而承认多项式霍恩重写。

概率系统中的频率LTL

On Frequency LTL in Probabilistic Systems

研究了频率线性时序逻辑（fLTL），它是线性时序逻辑（LTL）的扩展，引入了一个路径算子$G^p$，表示在一条路径上，某个公式至少对给定的频率p成立，从而放松了LTL常用的G算子的语义.这种逻辑在概率系统中特别有用，在概率系统中，一些不期望的事件（如随机故障）可能会发生，如果它们足够罕见，则是可以接受的。与频率相关的扩展LTL以前已经研究了几个作者，其中大多数逻辑配备了一个扩展的“直到”和“全球”运营商，导致最有趣的问题的不可判定性。对于我们研究的变体，我们能够建立基本的可判定性结果。我们表明，对于马尔可夫链，一个给定的fLTL公式持有的概率计算的问题具有相同的复杂性类似的问题LTL。我们还表明，马尔可夫决策过程的问题变得更加微妙，但当限制的频率范围$p$为1和否定不以外的任何$G^p$运营商，我们可以计算满足fLTL公式的最大概率。这可以再次以与普通LTL公式相同的时间复杂度来执行。

余代数动态逻辑的弱完备性

Weak Completeness of Coalgebraic Dynamic Logics

我们提出了Fischer和Ladner的命题动态逻辑（PDL）和Parikh的游戏逻辑（GL）的共代数概括。在早期的工作中，我们证明了一个通用的强完备性结果的余代数动态逻辑没有迭代。这些程序的共代数语义由单子T给出，模态通过谓词提升来解释，其转置是从T到邻域单子的单子态射。在本文中，我们表明，如果单子T进行了一个完整的半格结构，那么我们可以定义一个迭代构造，和适当的概念菱形和框状的谓词提升，允许定义的公理化参数在T中，pixel和一组选定的逐点程序操作。作为我们的主要结果，我们表明，如果逐点操作是“负自由”和Kleisli组合左分布在诱导加入Kleisli箭头，那么这个公理化是弱完全的标准模型类。作为特例，我们恢复了PDL和双自由博弈逻辑的弱完备性。作为一个适度的新的结果，我们获得了完整的双自由GL扩展与交叉（恶魔的选择）的游戏。

Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)

This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic, called LTLf Modulo Theories (LTLfMT), is semi-decidable. Nevertheless, its high expressiveness comes useful in a number of use cases, such as model-checking of data-aware processes and data-aware planning. Despite the general undecidability of these problems, being able to solve satisfiable instances is a compromise worth studying. After motivating and descri…

不完全信息和完全召回语义下的模型检验ATL是不可判定的

Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable

我们提出了一个形式化证明的不完全信息和完美召回语义下的交替时间时序逻辑的模型检验问题的不可判定性。这个问题被宣布为不可判定的根据个人通信的多人游戏与不完美的信息，但没有正式的证明曾经公布。我们的证明是基于直接减少从非停机问题的图灵机。

高表达描述逻辑的实用推理

Practical Reasoning for Very Expressive Description Logics

描述逻辑是一类知识表示形式化体系，其主要特征是构造器从原子概念和角色构造复杂的概念和角色。表达角色构造器在许多应用中很重要，但在计算上可能存在问题。我们提出了一个算法，决定可满足性的DL ALC扩展与传递和逆角色和功能限制方面的一般概念包含公理和角色层次结构，早期的实验表明，该算法是非常适合实施。此外，我们还证明了仅具有传递和逆角色的ALC扩展仍然是PSPACE中的。我们调查这个家庭的DL的可判定性的限制，表明放松限制放置在数量限制中使用的各种角色导致所有推理问题的不可判定性。最后，我们描述了一些优化技术，这是至关重要的，在获得实现的决策过程中，尽管最坏情况下的问题的复杂性，表现出良好的性能与现实生活中的问题。

具有策略上下文的ATL的可满足性

Satisfiability of ATL with strategy contexts

时态逻辑ATL的各种扩展最近被引入到表达多智能体系统的丰富属性。其中，ATLsc扩展了ATL的策略上下文，而策略逻辑具有一阶量化策略。这些逻辑的丰富表现力是有代价的：模型检查是非初等的，可满足性是不可判定的。本文证明了可满足性在几种特殊情况下是可判定的。最重要的一点是限制在回合制游戏中。我们证明，决策性也持有并发游戏，如果移动的数量可供代理是有界的。最后，我们证明了限制策略量化无记忆策略带来了不可判定性。

通过结构细化方法为直觉语法学逻辑构建嵌套序列为

Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement

本文通过结构细化方法，为直觉语法学逻辑构建了无割嵌套序列表演系统，并证明了其保守性、不可判定性和可判定子类。

元胞自动机轨道上的 FO 逻辑等价于 MSO 逻辑

FO logic on cellular automata orbits equals MSO logic

本文将经典元胞自动机扩展至任意标记图，证明其轨道上的 FO 逻辑等价于 MSO 逻辑，并据此推导出模型检测与可满足性的不可判定性结论及具体公式实例。

通过希尔伯特第十问题的不可判定性构造性证明里希的定理和停机问题

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

本文基于希尔伯特第十问题的不可判定性，通过双见证构造方法，构造性地证明了里希定理和停机问题的不可判定性，无需使用对角线法或自指。

当Lewis与Brouwer邂逅强Löb

Lewis and Brouwer meet Strong Löb

本研究在构造性Löb逻辑中考察“强度”原理，给出可证性逻辑核心定理的简化形式，证明两个系统的一致插值性，概述其算术解释并梳理与计算机科学的关联。

描述逻辑中的最小模型推理：别在家里尝试！

Minimal Model Reasoning in Description Logics: Don't Try This at Home!

本研究探讨描述逻辑中纯最小模型推理，发现EL中概念可满足性不可判定，通过无环性条件恢复可判定性，并证明DL-Lite_horn的ExpSpace难度。

有限可数模型下概率逻辑有效性和可满足性的可计算性

Computabilities of Validity and Satisfiability in Probability Logics over Finite and Countable Models

Kuyper和Terwijn的$ε$ -逻辑（本文中称为$ε$ E-逻辑）是一阶逻辑的变体，具有相同的语法，其中模型配备有概率测度，并且其中$\forall x$量词被解释为“存在测度$\ge 1 - ε$的集合$A$，使得对于每个$x \in A$，.在此之前，Kuyper和Terwijn证明了这个逻辑的一般可满足性和有效性问题是：i）对于有理$ε\in (0, 1)$，分别是$Σ^1_1$ -完全和$Π^1_1$ -困难的; ii）对于$ε= 0$，分别是可判定的和$Σ^0_1$ -完全的。形容词“普遍”在这里的意思是“在所有语言中一致”。“我们在有限模型的情况下扩展了这些结果。特别是，我们证明了在$ε$ E-逻辑有限模型的可满足性和有效性的问题，i）合理的$ε\in (0, 1)$，分别为$Σ^0_1$ -和$Π^0_1$ -完全，和ii）$ε= 0$，分别可判定和$Π^0_1$ -完全。虽然也取得了部分结果对可数的情况下，$ε$ E-逻辑的可计算性在可数模型仍然在很大程度上没有解决。此外，大多数的结果，本文和Kuyper和Terwijn，不适用于个别语言的有限数量的一元谓词。降低这一要求仍然是研究的重点。在积极的一面，我们得出了相应的问题的可判定性一元关系语言-平等和功能免费的语言与许多一元和零其他谓词。这一结果适用于所有三种无限制、可数和有限模型的情况。在这些可判定性和不…