If the formula is syntactically wrong, the system prints an error message.
If the formula is provable, its Proof is displayed in the Proof Window.
If the formula has an intuitionistic proof (without the Raa rule), this proof is given.
If the formula is not provable, the prover gives a counter-model
Annotate Proof
Data :a formula and a proof
If the formula is syntactically wrong, the system prints an error message.
If the proof has errors or does not prove the formula, the system gives a warning and open a
new window with the number of the Proof'line with the numeroted proof
If the proof is correct and proves the formula , the system open a
new window with the justified Proof