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 language | English |
---|---|
Title of host publication | PPDP '20: Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming |
Publisher | Association for Computing Machinery |
ISBN (Electronic) | 9781450388214 |
DOIs | |
Publication status | Published - Sept 2020 |
Event | 22nd International Symposium on Principles and Practice of Declarative Programming 2020 - Bologna, Italy Duration: 8 Sept 2020 → 10 Sept 2020 Conference number: 22 http://www.cse.chalmers.se/~abela/ppdp20/ |
Conference
Conference | 22nd International Symposium on Principles and Practice of Declarative Programming 2020 |
---|---|
Abbreviated title | PPDP 2020 |
Country/Territory | Italy |
City | Bologna |
Period | 8/09/20 → 10/09/20 |
Internet address |
ASJC Scopus subject areas
- Human-Computer Interaction
- Computer Networks and Communications
- Computer Vision and Pattern Recognition
- Software