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 S4translation is displayed.
If the formula is not provable, the prover gives a countermodel.
The prover is implemented in
Ocaml
.
examples

rules

syntax

info

home

download

basis of the method (in french)
Last Modified : 19Jan2018