ML Anthology

Formal Semantics and Formally Verified Validation for Temporal Planning

Mohammad Abdulaziz, Lukas Koller
AAAI 2022 pp. 9635-9643
doi:10.1609/AAAI.V36I9.21197 /aaai/2022/abdulaziz2022aaai-formal/

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.

PDF AAAI Semantic Scholar

Cite

Text

Abdulaziz and Koller. "Formal Semantics and Formally Verified Validation for Temporal Planning." AAAI Conference on Artificial Intelligence, 2022. doi:10.1609/AAAI.V36I9.21197

Markdown

[Abdulaziz and Koller. "Formal Semantics and Formally Verified Validation for Temporal Planning." AAAI Conference on Artificial Intelligence, 2022.](https://mlanthology.org/aaai/2022/abdulaziz2022aaai-formal/) doi:10.1609/AAAI.V36I9.21197

BibTeX

@inproceedings{abdulaziz2022aaai-formal,
  title     = {{Formal Semantics and Formally Verified Validation for Temporal Planning}},
  author    = {Abdulaziz, Mohammad and Koller, Lukas},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2022},
  pages     = {9635-9643},
  doi       = {10.1609/AAAI.V36I9.21197},
  url       = {https://mlanthology.org/aaai/2022/abdulaziz2022aaai-formal/}
}