Automatic generation of programs for proof animation

lIf a proof is
intuitionistic, namely does not use the principle of excluded middle
**A or
not A, **a program which execute the proof is automatically obtained.
Actually, the example of marbles is intuitionistic and, a skeleton of the applet could be
automatically generated.

lHowever, not for
classical proofs using **A or ****not A~{!-~}.**