FindComputation[rules, init, [dest], [what]]

Destination:
specific expression
pattern for expressions (analog of ∃)
meta-expression FixedPoint , loop , etc.

Generally: get to any multiway fragment that matches a certain multiway pattern

(this is a graph version of NestWhile etc.) [runnable on NDTM]

What:
Simply test if it’s possible
Give a path
Give multiple paths

ReplaceAt[rule,pos][expr]
Composition[ReplaceAt[rule,pos],ReplaceAt[rule,pos],ReplaceAt[rule,pos]][lhs]

FindComputation[function, ...]

Multi[XXXX]

In[]:=
unquantifyFormula[ForAll[{a,b},Exists[c,a==b⊙c]]]
Out[]=
a$1_b$5_⊙c$1[a$1_,b$5_]

When should built-in functions return Multi[ ]?

Computational graph defines the sequential/parallel computation