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.


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.
BSD License


Theories of AI_Planning_Languages_Semantics