Encodings based on state-based proofs

Propositions corresponding to initial

conditions and goals are true at their

respective levels

P1-0 & P2-0 & P7-k & P9-k

At least one of the actions at each level

will occur

a1-j V a2-J V … V an-j

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

Pi-j & Ak-(j+1) => Pi-j

forall Ak that don’t affect Pi

No more than one action occurs at

each step

~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 ..

Where al, am… add Pi

No pair of interacting actions must occur together

~aj-k V ~am-k forall k

forall aj,am that interfere

Regression (explanatory frame)

Progression (classical Frame)

O(k* (|O|+|U|)) variables

O(k*(|O| + |U|)) clauses