Prove Formula Data : a formula
  • If the formula is syntactically wrong, the system prints an error message.
  • If the formula is provable, its proof 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 Last Modified : 20-Nov-2019