Salomé Eriksson (University of Basel)
Gabriele Röger (University of Basel)
Malte Helmert (University of Basel)
Date: Tuesday 20 October 5 PM – 7 PM UTC
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.
The tutorial will be split in two parts with a 5 minute break in between.
Slides
helve on Github: https://github.com/salome-eriksson/helve