ICAPS 2020 Tutorial
Certified Unsolvability in Classical Planning
Salomé Eriksson, Gabriele Röger, Malte Helmert
ICAPS 2020, online
Tuesday, October 20, 2020, 19:00-21:00 CEST
Description
Asserting correctness is an important step in both academic research and practical applications for increasing trust in planning systems. For example, it has been a long standing practice in the International Planning Competition to validate all plans with an independent validator. With the recent increased interest in unsolvable planning tasks however, new validation tools are needed that are capable of verifying unsolvability claims. This tutorial presents one such tool based on a proof system approach, where unsolvability of a specific task is proven by iteratively expanding a knowledge base and applying deduction rules. In addition to presenting the overall philosophy and architecture of the proof system, we focus on the question how planning systems can emit proofs verifiable by the proof system. Participants are expected to have basic knowledge about classical planning but do not need any other background.
Outline
| 1. | Theoretical Foundations (PDF) (4in1) |
| 2. | Applications (PDF) (4in1) |
| 3. | Bibliography (PDF) (4in1) |