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 | formulas syntax | proofs definition | info | download | home Last Modified : 23-Feb-2023