Information
Prove Formula
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
Ocaml
.
examples
|
rules
|
syntax
|
info
|
home
|
download
|
basis of the method (in french)
Last Modified : 17-Dec-2021