英国曼彻斯特大学计算机科学系招收全奖博士
时态逻辑的定理证明
关于项目
时态逻辑对于指定和验证随时间变化的系统非常有用。
在文献[3]中，我们描述了一种基于归结法的命题线性时态逻辑（LTL）定理证明演算。其中，通过使用一种范式转换，减少了需要考虑的运算符数量，并且公式要么出现在初始状态中，要么在所有状态下都成立。该演算已在定理证明器TRP++[4]中实现。
本项目的目标是重新审视该演算及其实现，开发并分析改进和扩展方案，并将其应用于系统。具体建议如下：
在文献[8]中，我们开发并实现了一种基本模态逻辑K的归结演算，该演算不使用范式（范式构造的公式在初始状态或所有状态下成立），而是利用与初始状态的距离进行计算。这减少了需要应用的归结规则的数量，提高了证明器的效率。本项目旨在探究这种思路在多大程度上可应用于时态逻辑，因为时态逻辑模型可表示为初始前缀后接循环。
演算中较为耗时的部分是循环查找规则的实现。需重新考虑该规则并开发新的算法。
在文献[2]中，我们考虑添加“多个析取项中恰好一个成立”的运算符，这在指定系统时经常需要。本项目旨在将这种可能性添加到演算及其实现中。
度量时态逻辑（MTL）允许LTL中的时态运算符具有其成立的区间。在文献[5]中，我们考虑了从时态逻辑的自然数模型到LTL的不同转换，并进行了相关实验。与之相关的一种逻辑是任务时间时态逻辑[6]。本扩展项目旨在为其中一种逻辑的自然数模型开发演算，并实现和分析该演算。
FRET是一种规范工具[1]，可通过特定语言输入时态公式。本项目旨在扩展该工具，使其能够传递给一个或多个时态证明器，以检查规范的可满足性，并向用户提供反馈。
申请资格
申请人应已获得或预期获得相关科学或工程学科2.1及以上荣誉学位或硕士学位（或国际同等学历）。
资助信息
优秀候选人将被提名申请基于能力的院系资助（院系资助申请截止日期为2025年12月19日。若12月未收到合适申请，则将考虑于2026年3月13日截止的下一轮申请）。资助涵盖学费，并提供基于英国研究与创新署（UKRI）费率的无税津贴（2025/26学年为20,780英镑）。我们预计津贴每年会有所增长。该资助面向英国本土和海外候选人。我们建议您尽早申请，因为广告可能会在截止日期前撤下。
项目开始日期为2026年10月。
在曼彻斯特大学，我们提供大学、院系和部门层面的奖学金、研究助学金和奖项，以支持英国本土和海外的研究生研究人员。
如需更多信息，请访问我们的资助页面，或在我们的资助数据库中搜索您可能有资格申请的具体奖学金、研究助学金和奖项。
我们建议您尽早申请，因为广告可能会在截止日期前撤下。
申请前
我们强烈建议您在申请前联系本项目的导师。申请时，请提供您当前的学习水平、学术背景和任何相关经验，并附上一段关于您申请该博士项目动机的说明。
如何申请
请通过我们的网站在线申请：https://uom.link/pgr-apply-2425
申请时，您需要指定本项目的全称、导师姓名（如果您已获得资助或希望申请大学的资助）、先前学习经历的详细信息，以及两位推荐人的姓名和联系方式。
若未在申请时提交所有必需文件，您的申请将不予处理。我们不对逾期或错过截止日期的申请负责。不完整的申请将不予考虑。
申请后，您将被要求上传以下支持文件：
所有已授予的大学水平学历的最终成绩单和证书
正在攻读的任何大学水平学历的临时成绩单
简历
支持声明：一份一至两页的声明，概述您攻读研究生研究的动机、为何选择在曼彻斯特大学攻读研究生研究、任何相关研究或工作经验、先前研究经验的关键发现，以及您所掌握的技术和技能。（所有申请人均需提交此声明，否则申请将被搁置。）
两位推荐人的联系方式（请确保您提供的联系邮箱为官方大学/工作邮箱，因为我们可能需要验证推荐信。）
英语语言证书（如适用）
如对申请有任何疑问，请通过电子邮件FSE.doctoralacademy.admissions@manchester.ac.uk联系#我们的招生团队。
平等、多样性和包容性是曼彻斯特大学成功的基石，也是我们所有活动的核心。我们知道，多样性能够增强我们的研究社区，提高研究创造力、生产力和质量，以及社会和经济影响力。
我们积极鼓励来自不同职业道路和背景以及社会各界的申请人申请，无论其年龄、残疾、种族、性别、性别表达、性取向和跨性别身份如何。
我们还支持从职业中断或其他角色中回归的申请人申请。我们考虑提供灵活的学习安排（包括兼职：50%、60%或80%，具体取决于项目/资助方）。
参考文献
[1] Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Julian Rhein, Johann Schumann, Nija Shi, Formal Requirements Elicitation with FRET, REFSQ Workshops 2020[2] Dixon, C., Konev, B., Fisher, M. and Nietiadi, S., Deductive temporal reasoning with constraints, Journal of Applied Logic. 11, 1, p. 30-51, 2013[3] Fisher, M., Dixon, C. & Peim, M., 2001, Clausal Temporal Resolution, ACM Transactions on Computational Logic.[4] Hustadt, U and Konev, B, TRP++2.0: A Temporal Resolution Prover. CADE 2003: 274-278[5] Hustadt, U., Ozaki, A. & Dixon, C., Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations Journal of Automated Reasoning. 64, 8, p. 1553-1610, 2020[6] Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time ltl (mltl). Information and Computation 289, 104923 (2022)[7] Nalon, C., Hustadt, U. & Dixon, C., A Resolution-Based Theorem Prover for Kn, Kn: Architecture, Refinements, Strategies and Experiments Journal of Automated Reasoning, 2020[8] Nalon, C., Dixon, C. & Hustadt, U., Modal Resolution: Proofs, Layers and Refinements ACM Transactions on Computational Logic. 20, 4, 23, 2019.
【竞赛报名/项目咨询+微信：mollywei007】
