- 编码器 - 只有 Transformer 的形式推理的计算复杂性
研究了编码器 - 只有变压器 (EOT) 的形式化推理的挑战和可能性，发现 EOT 的满足性问题 (SAT) 是不可判定的，但限定了注意力能力的量化 EOT 可以在 NEXPTIME 内解决 SAT 问题。
- Petri 网中的双可达性
我们研究了带有数据的 Petri 网，Petri 网的扩展，其中令牌携带来自无限数据域的值，并且过渡的可执行性取决于数据值之间的等式。我们提供了一个双向可达性问题的决策过程：给定一个 Petri 网及其两个配置，我们询问每个配置是否可以从另 - 语义方法在认知规划中的可决定性（扩展版）
利用动态认知逻辑（DEL）的多代理规划在处理非确定性、部分可观察性和任意知识嵌套方面具有广泛应用的行动形式主义中，我们通过一种新颖的语义方法达到可决定性的目标。我们展示了该框架具有可决定的特性，并研究了其他扩展的交换公理以实现更复杂的 DE - 探索命题动态逻辑的非正则扩展与描述逻辑特征
在扩展 ALC 描述逻辑的决定性满足性检查和查询中，我们研究了非规则路径表达式的影响。我们重点研究了 ALCreg 和 ALCvpl，它们是使用正则和可见推动语言的路径表达式的扩展。
- 带有抽象和细化功能的描述逻辑
提出一种将抽象级别作为一等公民并提供概念和角色的抽象和细化的显式运算符的 DLs 扩展，它可以支持多个抽象级别上的知识表示，并证明在这个扩展的 DLs 家族中推理是可判定的，而一些看似无害的变化则是不可判定的。
- 连接证明理论和知识表示：序列演算和具有存在规则的 Chase
本文主要探讨了知识表示中重要的可决定性工具 ——Chase 算法与证明理论中的证明搜索算法之间的联系，特别是在一阶逻辑的 Gentzen 序列演算的推广中探究了在存在性规则的情况下 Chase 机制本质上与证明搜索相同，并通过证明搜索生成知 - 指针程序序列的分离逻辑及其可判定性
我们提出了序列堆分离逻辑，将序列集成到堆操纵程序的逻辑推理中，该逻辑包括序列变量量词和存储序列的单例堆。我们研究了序列堆分离逻辑的两个片段的可满足性问题，并探讨了正前式正规形式的解释逻辑边界。
- 存在规则的有限团宽集：朝着决定性、高表达性查询的通用准则迈进
该研究通过引入 “有限团宽集合”（FCS）来寻求可决定本体论查询的一般性标准，FCS 是一种模型理论定义的规则集类，受到图论中团宽的启发，这一类规则集确保了一类子句共有查询（DaMSOQs）的蕴涵可决定性，它们吸收了合取查询（CQs）并且限 - 使用传递性和线性排序数据进行查询回答
本研究研究了涉及强约束语言的蕴涵问题，如前沿守卫存在规则，并对一组特殊的关系施加额外的语义限制。我们考虑将关系限制为传递性、将一个关系的传递闭包限制为另一个关系、将关系限制为线性顺序。我们提出了一些自然的守卫性变体，以使推理在每种情况下具有 - MM追逐变种中的有界性特征
研究论文探讨了基于本体的查询应答中的万有模型问题，特别关注存在规则边界问题，提出了一般性质并证明了一些经典的 chase 变体满足该性质，进而解决了这些变体的有限深度问题。
- 定性数值规划：简化与复杂性
本文研究定性数量规划问题，提出了两种多项式时间降阶方法，将问题转化为非确定性计划问题和反之，从而解决解决方案不完整问题和复杂度问题。
- Existential 规则的 k-Boundedness 问题
该论文研究对于三种追赶算法变种，如何确定给定规则集的有界性问题是可决的。
- AAAI带有有限 Chase 的存在规则语言：复杂度和表达能力
本文通过对具有有限追赶特性的规则语言分类，提出了一族可决定性规则语言，研究了这些语言的复杂性，证明了具有有限追赶特性的规则语言扩展弱无环语言的表现力与弱无环语言相同，并且综合复杂性更高的规则语言一般比综合复杂性更低的规则语言更简洁。
- 验证关系型数据中心动态系统与外部服务
本文研究基于关系型数据中心动态系统的（一阶）μ 演算验证，展示了在一些特殊情况下可决定性成立，并提供了一些避免不可决情况的句法条件，构建了一些注意到每个服务调用激活会生成新值的新概念以避免无限积累问题。
- 位移微积分
本文介绍了位移演算为 Lambek 演算的一般化，它保留了 Lambek 演算的证明论特性，同时将不连续性融合到其中，并涵盖了它。我们举例说明语言应用，并证明减少消除，子公式属性和可决定性。