Proof-Carrying Plans: a Resource Logic for AI Planning

Research output: Chapter in Book/Report/Conference proceedingConference contribution

184 Downloads (Pure)

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. Keywords: AI planning, Verification, Resource Logics, Theorem Proving, Dependent Types.
Original languageEnglish
Title of host publicationPPDP '20: Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming
PublisherAssociation for Computing Machinery
ISBN (Electronic)9781450388214
DOIs
Publication statusPublished - Sept 2020
Event22nd International Symposium on Principles and Practice of Declarative Programming 2020 - Bologna, Italy
Duration: 8 Sept 202010 Sept 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
Country/TerritoryItaly
CityBologna
Period8/09/2010/09/20
Internet address

ASJC Scopus subject areas

  • Human-Computer Interaction
  • Computer Networks and Communications
  • Computer Vision and Pattern Recognition
  • Software

Fingerprint

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

Cite this