日程冲突检测算法建模及自动化验证方法

摘要

日程冲突检测算法在会议管理、教学排课和医疗排班等场景中具有重要价值，其核心问题可抽象为时间区间的重叠检测．区间树作为典型的区间查询结构，能够高效支持插入、删除与查询操作，因此区间树成为实现该类算法的理想选择．为确保算法的可靠性与可扩展性，该文基于区间树构建了函数式建模库，并完善了配套的验证引理库，以保证其基本操作在严格形式化语义下的正确性．在此基础上，进一步完成了日程冲突检测算法的形式化建模与自动化验证实验，依托所构建的建模库与验证引理库，算法的功能与结构正确性能够借助自动化证明工具完成验证，从而有效地降低了人工证明成本，验证了所给方法的可行性与有效性．

关键词

日程冲突检测 / 区间树 / Isabelle定理证明器 / 函数式建模 / 自动化验证

基金资助

国家自然科学基金(62462036); 江西省自然科学基金(20242BAB26017)资助项目