BriefGPT.xyz
Mar, 2022
时态规划的形式语义与形式验证
Formal Semantics and Formally Verified Validation for Temporal Planning
HTML
PDF
Mohammad Abdulaziz, Lukas Koller
TL;DR
该研究在交互式定理证明器Isabelle/HOL中，提出了一种简单而简洁的时间规划语义，并基于该语义推导了验证算法。通过正式证明，该验证算法实现了时间规划语义，并进行了实验评估，证明其实用性。
Abstract
We present a simple and concise
semantics
for
temporal planning
. Our
semantics
are developed and formalised in the logic of the
→