Encodings based on Causal proofs

Each step is mapped to exactly one action

Si = A1 V Si = A2 … ; ~( Si = Ai & Si = Aj)

A step inherits the needs, adds and deletes of the action it is mapped to

Si = Aj => Adds(Si, Pa) & Needs(Si, Pp) &

Deletes(Si, Pd)

A Step get needs, adds and deletes only through mapped actions

Adds(Si, Pa) => Si = Aj V Si = Ak …

(Ai, Ak add Pa)

Every need is established by some step

Needs(Si,Pj) => Estab(S1, Pj, Si) V

Estab(S2, Pj, Si) … V Estab(Sk, Pj, Si)

Establishment with causal links

Estab(S1,Pj,Si) => Link(S1,Pj,Si)

Link implies addition & precedence

Link(Si,Pj,Sk) => Adds(Si,Pj) &

Precedes(Si,Pj)

Link implies preservation by intervening steps

Link(Si,Pj,Sk) & Deletes(Sm,Pj)

=> Precedes(Sm, Si) V

Precedes(Sk, Si)

Precedence is irreflexive, asymmetric and transitive...

O(k2* |U|) causal link variables

O(k3 *|U|)) Threat resolution clauses

[Kautz, McAllester, Selman, 96]