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

Prerequisites:
Experience with Isabelle/HOL is required.
Advisor:
Mohammad Abdulaziz, email {mansour} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]

Material to read:

[1]
A textbook on planning by Malik Ghallab, Dana Nau, and Paolo Traverso: http://projects.laas.fr/planning/book.pdf
[2]
Paper on pattern databases: https://pdfs.semanticscholar.org/f17a/8d6aaa9a876cc1e48afb22ba6d312f14d307.pdf
[3]
Paper on pattern databases: http://idm-lab.org/bib/abstracts/papers/aaai07b.pdf
[4]
Papers on Merge-and-shrink https://dl.acm.org/citation.cfm?id=2559951