Email Gateway (Nov 13 2020 at 13:24): Email Gateway (Nov 13 2020 at 13:24):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce a pair of related submissions:
AI Planning Languages Semantics
Mohammad Abdulaziz and Peter Lammich
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.
https://www.isa-afp.org/entries/AI_Planning_Languages_Semantics.html
And also
Verified SAT-Based AI Planning
Mohammad Abdulaziz and Friedrich Kurz
We present an executable formally verified SAT encoding of classical AI planning that is based on the encodings by Kautz and Selman and the one by Rintanen et al. The encoding was experimentally tested and shown to be usable for reasonably sized standard AI planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths. The formalisation in this submission was described in an independent publication.
https://www.isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html
Larry Paulson
Last updated: Jul 15 2022 at 23:21 UTC