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 : 19-Jan-2018