一句话：研究守卫等可判定不动点逻辑中公式可定义性与插值，通过树模型性质及关系/树逻辑转换给出语义与有效刻画。
论文研究如何在若干富有表达力但仍可判定的不动点逻辑中刻画公式的可定义性，覆盖守卫不动点逻辑、一元否定不动点逻辑和守卫否定不动点逻辑。作者同时考察可定义性的语义刻画与有效刻画，并讨论插值问题。方法上，论文更精细地分析这些逻辑的树模型性质，并改进在关系逻辑与树逻辑之间往返转换的技术，从而把可定义性与插值的研究扩展到强于经典模态/时序逻辑的守卫式不动点框架。评估以理论证明和算法构造为主，摘要未报告实验或实现。
We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back and forth between relational logics and logics over trees.
@article{paperbot756,
title = {Definability and Interpolation within Decidable Fixpoint Logics},
author = {Michael Benedikt and Pierre Bourhis and Michael Vanden Boom},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 3},
year = {2019},
doi = {10.23638/lmcs-15(3:29)2019}
}