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.
BSD LicenseTopics
Theories of AI_Planning_Languages_Semantics
- Error_Monad_Add
- Option_Monad_Add
- SASP_Semantics
- SASP_Checker
- PDDL_STRIPS_Semantics
- PDDL_STRIPS_Checker
- Lifschitz_Consistency