### 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

- Computer science/Artificial intelligence

### Session AI_Planning_Languages_Semantics

- Error_Monad_Add
- Option_Monad_Add
- SASP_Semantics
- SASP_Checker
- PDDL_STRIPS_Semantics
- PDDL_STRIPS_Checker
- Lifschitz_Consistency

### Depends on

- Certification Monads
- Light-weight Containers
- Propositional Proof Systems
- Haskell’s Show Class in Isabelle/HOL

### Used by

- Verified SAT-Based AI Planning

## Cite

×

AI_Planning_Languages_Semantics-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Oct 30, 2020 : Isabelle2020