Mechanising Theoretical Upper Bounds in Planning

Mohammad Mansour (Abdulaziz); Charles Gretton; Michael Norrish

Mechanising Theoretical Upper Bounds in Planning

Mohammad Mansour (Abdulaziz), Charles Gretton, Michael Norrish

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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

Original language	English
Title of host publication	Proceedings of the Twenty-Fourth International Conference on Automated Planning and Scheduling
Editors	S Chien, A Fern, W Ruml, M Do
Place of Publication	USA
Publisher	Association for the Advancement of Artificial Intelligence (AAAI)
Pages	1 - 7pp
Edition	peer reviewed
ISBN (Print)	9781577356608
Publication status	Published - 2015
Event	24th International Conference on Automated Planning and Scheduling 2014 (ICAPS) - Portsmouth, USA Duration: 21 Jun 2014 → 26 Jun 2014 http://www.aaai.org/Library/ICAPS/icaps14contents.php

Conference

Conference	24th International Conference on Automated Planning and Scheduling 2014 (ICAPS)
Period	21/06/14 → 26/06/14
Other	June 21-26 2014
Internet address	http://www.aaai.org/Library/ICAPS/icaps14contents.php

Cite this

@inproceedings{e6ef0fd2073048fe8a830984072ea991,

title = "Mechanising Theoretical Upper Bounds in Planning",

abstract = "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",

author = "{Mansour (Abdulaziz)}, Mohammad and Charles Gretton and Michael Norrish",

year = "2015",

language = "English",

isbn = "9781577356608",

pages = "1 -- 7pp",

editor = "{S Chien, A Fern, W Ruml, M Do}",

booktitle = "Proceedings of the Twenty-Fourth International Conference on Automated Planning and Scheduling",

publisher = "Association for the Advancement of Artificial Intelligence (AAAI)",

edition = "peer reviewed",

note = "24th International Conference on Automated Planning and Scheduling 2014 (ICAPS) ; Conference date: 21-06-2014 Through 26-06-2014",

url = "http://www.aaai.org/Library/ICAPS/icaps14contents.php",

}

Mansour (Abdulaziz), M, Gretton, C & Norrish, M 2015, Mechanising Theoretical Upper Bounds in Planning. in SCAFWRMD (ed.), Proceedings of the Twenty-Fourth International Conference on Automated Planning and Scheduling. peer reviewed edn, Association for the Advancement of Artificial Intelligence (AAAI), USA, pp. 1 - 7pp, 24th International Conference on Automated Planning and Scheduling 2014 (ICAPS), 21/06/14.

Mechanising Theoretical Upper Bounds in Planning. / Mansour (Abdulaziz), Mohammad; Gretton, Charles; Norrish, Michael.
Proceedings of the Twenty-Fourth International Conference on Automated Planning and Scheduling. ed. / S Chien, A Fern, W Ruml, M Do. peer reviewed. ed. USA: Association for the Advancement of Artificial Intelligence (AAAI), 2015. p. 1 - 7pp.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Mechanising Theoretical Upper Bounds in Planning

AU - Mansour (Abdulaziz), Mohammad

AU - Gretton, Charles

AU - Norrish, Michael

PY - 2015

Y1 - 2015

N2 - 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

AB - 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

M3 - Conference contribution

SN - 9781577356608

SP - 1

EP - 7

BT - Proceedings of the Twenty-Fourth International Conference on Automated Planning and Scheduling

A2 - null, S Chien, A Fern, W Ruml, M Do

PB - Association for the Advancement of Artificial Intelligence (AAAI)

CY - USA

T2 - 24th International Conference on Automated Planning and Scheduling 2014 (ICAPS)

Y2 - 21 June 2014 through 26 June 2014

ER -

Mechanising Theoretical Upper Bounds in Planning

Abstract

Conference

Fingerprint

Cite this