Data : a formula of propositional intuitionistic logic
If the formula is syntactically wrong, the system prints an error message.
If the formula is provable, the proof of its S4-translation is displayed.
If the formula is not provable, the prover gives a counter-model.
The prover is implemented in
basis of the method (in french)
Last Modified : 19-Jan-2018