Encodings based on state-based proofs
Propositions corresponding to initial
conditions and goals are true at their
P1-0 & P2-0 & P7-k & P9-k
At least one of the actions at each level
Actions imply their preconditions and effects
ai-k => precai-k-1 & Effai-k
A proposition P at j remains true if
no action occuring at j+1 deletes P
forall Ak that don’t affect Pi
No more than one action occurs at
~aj-k V ~am-k forall j,m,k
A proposition P changes values
between j and j+1 only if an action occurs that makes it so
~Pi-j & Pi-(j+1) => al-j V am-j ..
No pair of interacting actions must occur together
forall aj,am that interfere
Regression (explanatory frame)
Progression (classical Frame)
O(k* (|O|+|U|)) variables