Information

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 in the Proof Window.
    If the formula has an intuitionistic proof (without the Raa rule), this proof is given.
  • If the formula is not provable, the prover gives a counter-model
Annotate Proof Data :a formula and a proof
  • If the formula is syntactically wrong, the system prints an error message.
  • If the proof has errors or does not prove the formula, the system gives a warning and open a new window with the number of the Proof'line with the numeroted proof
  • If the proof is correct and proves the formula , the system open a new window with the justified Proof

The prover is implemented in Ocaml.

examples | rules | syntax | info | download | home Warning: date(): It is not safe to rely on the system's timezone settings. You are *required* to use the date.timezone setting or the date_default_timezone_set() function. In case you used any of those methods and you are still getting this warning, you most likely misspelled the timezone identifier. We selected 'Europe/Berlin' for 'CEST/2.0/DST' instead in /www/html/membres/michel.levy/prover/footer.inc on line 13 Last Modified : 21-Oct-2009