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.

You can find the theoritical basis for this prover in the following paper written by Vìtězlav Švejdar.
The prover is implemented in Ocaml.

examples | rules | syntax | info | home | download

Last Modified : 17-Dec-2021