Skip to main content


Mechanising theoretical upper bounds in planning


Mohammad Abdulaziz, Charles Gretton and Michael Norrish


Australian National University

Griffith University


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 primary contribution is to identify and repair an important error in the original formalisation of bounds. We also develop novel bounding results and compare them analytically with existing bounds.

BibTeX Entry

    author           = {Abdulaziz, Mohammad and Gretton, Charles and Norrish, Michael},
    month            = {jun},
    slides           = {},
    year             = {2014},
    keywords         = {automated planning, upper bounds},
    title            = {Mechanising Theoretical Upper Bounds in Planning},
    booktitle        = {Workshop on Knowledge Engineering for Planning and Scheduling},
    address          = {Portsmouth, USA}