研究了具有数字限制的 SQ 描述逻辑，该逻辑适用于传递性角色，并扩展为名词或反向角色。为 nominals 的正存在查询和为 inverses 的实例查询建立了上界。

Oct, 2020

本研究研究了涉及强约束语言的蕴涵问题，如前沿守卫存在规则，并对一组特殊的关系施加额外的语义限制。我们考虑将关系限制为传递性、将一个关系的传递闭包限制为另一个关系、将关系限制为线性顺序。我们提出了一些自然的守卫性变体，以使推理在每种情况下具有可决定性，并确定了相应决策问题的复杂度。最后，我们证明了这些条件的轻微变化会导致不可决定性问题。

Feb, 2022

本文探讨存在规则作为本体规范的形式化方法，重点研究了如何将传递性与可判定类的存在规则组合，并给出了能够安全添加传递性的情况和相应的查询重写算法。

Apr, 2015

对于带计数的两变量片段的可满足性和有限可满足性问题的数据复杂度为 NP - 完全；对于带计数的两变量受限片段的查询回答和有限查询回答问题的数据复杂度为 co-NP - 完全。

Jun, 2008

研究了 Timed Propositional Temporal Logic (TPTL) 的 {0，∞} 分片的可决定性，并证明 TPTL^ {0，∞} 的可满足性检查为 PSPACE-complete。此外，即使是它的 1 变量分片（1-TPTL^ {0，∞}）也比 Metric Interval Temporal Logic (MITL) 更具表达能力，后者的可满足性检查是 EXPSPACE complete。因此，我们拥有更加表达能力的逻辑并具有较简单的可满足性检查。据我们所知，TPTL^ {0，∞} 是第一个多变量 TPTL 分片，其可满足性检查在没有对时态词（如时间可变性，时间有界性等）施加任何限制的情况下是可决定的。PSPACE 的成员关系是通过将其规约到一种名为 Unilateral Very Weak Alternating Timed Automata (VWATA^ {0，∞}) 的新 “非确定性” 时态自动机的空泛性检查问题获得的，我们证明了这个问题在 PSPACE 中。通过构造一个与给定 VWATA^ {0，∞} 的大小多项式相关的非确定性时态自动机的模拟等价关系来证明这一点。

Sep, 2023

本文研究了有限结构中存在性正公式的答案数量计数问题，并在有界性条件下给出了关于查询类的三分定理，统一和泛化了关于合取查询和合取查询并的复杂性的已知结果。

Jan, 2016

本文研究了提供复合命题演绎的可能性，并通过引入几个扩展后的逻辑来分析是否需要将归谬法视为必要条件，得出了关于其存在（或不存在）的命题证明体系的结果，并确定了所有分段思维的计算复杂度。

Aug, 2008

提出了一个通用的查询决策框架，基于计数模型的结构简单性，可以确定各种逻辑蕴涵问题（简称查询）的可决性，其中 Blumensath 的分区宽度作为一个特别强大的宽度度量提出，重点介绍存在规则的形式化，其中分区宽度的规则子域覆盖范式为一周围侧子域。

Apr, 2023

本文研究了扩展时序约束问题的复杂性，并针对一组量词自由的 “小于等于（leq）” 公式所形成的 Poset-SAT 问题进行了讨论。其问题是对于 $x_1$，$x_2$，…，$x_n$ 成为偏序集时是否存在满足给定公式的赋值。最后，作者使用模型理论概念和通用代数技术研究了这些问题的约束满足问题，并提出了独立于通用代数和模型理论的分裂定理。

Feb, 2016

通过 Universal Dependencies 标记 negation scope 的能力，实现 UDepLambda 和 higher-order type theory 结合，处理代表否定、全称量词等复杂语义现象。初步实现针对英语的转化表现良好。

Feb, 2017