These softwares are made available to all, with the support of the VERIMAG laboratory.

- Propositional natural deduction Given a formula, the software builds a proof or an interpretation that falsifies it.
- Proof in first order logic by resolution Given a list of clauses, as well as limits on the time of proof and the size of the clauses, the software tries to build a proof of the empty clause within the imposed limits.
- Proof in first order logic by the Model Elimination method Given a list of clauses, as well as limits on the time and length of proof, the software tries to build a proof by this method.
- Tableaux method for modal logic S4 Given a formula, the software builds a proof by the tableaux method or an interpretation falsifying it.
- Tableaux method for intuitionist logic Given a formula, the software translates the formula into a S4-formula and either builds a proof of its translation into S4 or provides a falsifying interpretation.
- Proof in the sequent calculus for modal logic GL Given a formula, the software builds a proof by the Švejdar method or an interpretation that falsifies it.

Given a formula and proof, the software annotates the proof by indicating the rules applied.