AI Planning Languages Semantics

Mohammad Abdulaziz 🌐 and Peter Lammich 🌐

October 29, 2020


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


Session AI_Planning_Languages_Semantics