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

Last Modified : 17-Jan-2010