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