Proof-Carrying Plans: a Resource Logic for AI Planning

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

Abstract

Planning languages have been used successfully in AI for several decades. Recent trends in AI verification and Explainable AI have raised the question of whether AI planning techniques can be verified. In this paper, we present a novel resource logic, the Proof Carrying Plans (PCP) logic that can be used to verify plans produced by AI planners. The PCP logic takes inspiration from existing resource
logics (such as Linear logic and Separation logic) as well as Hoare logic when it comes to modelling states and resource-aware plan execution. It also capitalises on the Curry-Howard approach to logics, in its treatment of plans as functions and plan pre- and post-conditions as types. This paper presents two main results. From the theoretical perspective, we show that the PCP logic is sound relative to the standard possible world semantics used in AI planning. From the practical perspective, we present a complete Agda formalisation of the PCP logic and of its soundness proof. Moreover, we showcase the Curry-Howard, or functional, value of this implementation by supplementing it with the library that parses AI plans into Agda’s proofs automatically. We provide evaluation of this library and the resulting Agda functions.
Original languageEnglish
Title of host publication22nd International Symposium on Principles and Practice of Declarative Programming (PPDP ’20), September 8–10, 2020, Bologna, Italy.
PublisherAssociation for Computing Machinery
Publication statusAccepted/In press - 4 Aug 2020
Event22nd International Symposium on Principles and Practice of Declarative Programming 2020 - Bologna, Italy
Duration: 8 Sep 202010 Sep 2020
Conference number: 22
http://www.cse.chalmers.se/~abela/ppdp20/

Conference

Conference22nd International Symposium on Principles and Practice of Declarative Programming 2020
Abbreviated titlePPDP 2020
CountryItaly
CityBologna
Period8/09/2010/09/20
Internet address

Fingerprint Dive into the research topics of 'Proof-Carrying Plans: a Resource Logic for AI Planning'. Together they form a unique fingerprint.

  • Cite this

    Hill, A., Komendantskaya, E., & Petrick, R. P. A. (Accepted/In press). Proof-Carrying Plans: a Resource Logic for AI Planning. In 22nd International Symposium on Principles and Practice of Declarative Programming (PPDP ’20), September 8–10, 2020, Bologna, Italy. Association for Computing Machinery.