Mechanising Theoretical Upper Bounds in Planning
Mohammad Abdulaziz, Charles Gretton, Michael Norrish · International Conference on Automated Planning and Scheduling · 2014
We examine the problem of computing upper bounds on the lengths of plans. Tractable approaches to calculating such bounds are based on a decomposition of state-variable dependency graphs (causal graphs). Our contribution follows an existing formalisation of concepts in that setting, reporting our efforts to mechanise bounding inequalities in HOL. Our first contribution is to identify and repair an important error in the original formalisation of bounds. More importantly, we also develop novel theoretical bounding results and compare them analytically with existing bounds.