论文标题
正式的语义和正式验证时间计划的验证
Formal Semantics and Formally Verified Validation for Temporal Planning
论文作者
论文摘要
我们为时间计划提供了一种简单简洁的语义。我们的语义是在互动定理供奉献isabelle/hol的逻辑中开发和形式化的。我们从这些语义中得出了一种用于时间计划的验证算法，并使用Isabelle/Hol中的正式证明显示了该验证算法实现我们的语义。我们通过实验评估我们经过验证的验证算法，并表明它是实用的。
We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal planning and show, using a formal proof in Isabelle/HOL, that this validation algorithm implements our semantics. We experimentally evaluate our verified validation algorithm and show that it is practical.
