Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: AI planning

view this post on Zulip Email Gateway (Nov 13 2020 at 13:24):

From: Lawrence Paulson <>
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.

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.

Larry Paulson

Last updated: Jan 25 2022 at 01:11 UTC