Formalizing Unsolvability Certificates for Automated Planning in Lean 4
Amos Nicodemus

Abstract:
The objective of classical planning is to find a sequence of actions which leads from an initial state to a goal. Several solvers for automatically solving these planning problems exist, which either return a plan (such a sequence of actions) or state that no plan exists. In the latter case, we would want to verify that in fact there does not exist a plan, which can be done using certificates of unsolvability. Recently, two certificate systems have been developed, namely inductive certificates [19, 12] and a rule based proof system [18, 12]. The simplest version of an inductive certificate is a set of states that is closed under taking actions and contains the initial state but no goal state. The rule based proof system consists of rules to reason about sets of dead states, where a state is dead if no plan traverses the state.
Eriksson has implemented a validator based on this proof system in C++ [14]. Like any other software, this validator can have bugs, hence it would be useful to have a formally verified validator. The goal of the thesis is to implement a validator in Lean 4 for this proof system.