IJCAI 19

Full paper

Section: Framework, generic defs & motivation (Joerg + Dan)

• Plan property: polytime Boolean fn of task and action sequence vec_a
• Atomic dependency: for every vec_a if p is true then q is true
• Composed dependency: propositional formula over plan props. Motivation: this could be inside a single new plan prop. However, plan props are black boxes to the framework; in the exploration of composed dependencies, the explanation facility will establish the interesting combinations across these boxes

Motivate framework with examples, from proposal + extended/elaborated

Dependency phi holds if, for all action sequences, phi evaluates to true.

Entailment over two dependencies phi and psi: phi entails psi if, for every action sequence, if phi evaluates to true then so does psi

computational problems that we solve:

1. atomic: find all pairwise deendencies e graph whiose nodes are properties and whose edges are atomic dependencies
2. general: find all strongest dependencies: the root nodes in the DAG over equivalence classes of dependencies

show that dependencies, and entailment thereover, are more than standard propositional logic: even if a formula is not universally true, iot may be true for all action sequences due to the underlying planning task. In fact this will typically be the case, e.g. in a simple mutex where reaching one fact A excludes reaching another fact B.

Section Simple Instantiation goal-set conflicts

as per draft (Rebecca + Michael)

Section Compilation into goal-set conflicts

more general plan props and how they can be compiled into previous.

Section experiments

on simple instantiation as discussed, on compiled more general props.