Verified state space based classical planning

Chair for Logic and Verification

Master’s practical course, Master’s thesis, or IDP

State space search is a successful technique to solve classical AI planning problems, i.e. deterministic problems with finite states. The main task of this project is to (partially) build a formally verified A* based planning algorithm. Tasks in this project include

Experience with Isabelle/HOL is required.

Mohammad Abdulaziz, email {mansour} AT []

Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT []

Material to read:

A textbook on planning by Malik Ghallab, Dana Nau, and Paolo Traverso:

Paper on pattern databases:

Paper on pattern databases:

Papers on Merge-and-shrink