Formal Semantics and Formally Verified Validation for Temporal Planning

Mohammad Abdulaziz; Lukas Koller

AAAI 2022technical6 citations

Formal Semantics and Formally Verified Validation for Temporal Planning

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.

BibTeX

@inproceedings{aaai2022_formalsemanticsa,
  title = {Formal Semantics and Formally Verified Validation for Temporal Planning},
  author = {Mohammad Abdulaziz and Lukas Koller},
  booktitle = {AAAI 2022},
  year = {2022}
}