AI Planning Languages Semantics

Mohammad Abdulaziz 🌐 and Peter Lammich 🌐

October 29, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This is an Isabelle/HOL formalisation of the semantics of the multi-valued planning tasks language that is used by the planning system Fast-Downward, the STRIPS fragment of the Planning Domain Definition Language (PDDL), and the STRIPS soundness meta-theory developed by Vladimir Lifschitz. It also contains formally verified checkers for checking the well-formedness of problems specified in either language as well the correctness of potential solutions. The formalisation in this entry was described in an earlier publication.

License

BSD License

Topics

Session AI_Planning_Languages_Semantics

Depends on

Used by

Cite

× 
@article{AI_Planning_Languages_Semantics-AFP,
  author  = {Mohammad Abdulaziz and Peter Lammich},
  title   = {AI Planning Languages Semantics},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/AI_Planning_Languages_Semantics.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: