Proceedings:
No. 9: AAAI-22 Technical Tracks 9
Volume
Issue:
Proceedings of the AAAI Conference on Artificial Intelligence, 36
Track:
AAAI Technical Track on Planning, Routing, and Scheduling
Downloads:
Abstract:
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.
DOI:
10.1609/aaai.v36i9.21197
AAAI
Proceedings of the AAAI Conference on Artificial Intelligence, 36