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

- Propositional Natural Deduction

The basis of the three software below, is described in this document (only in french).- Propositional natural deduction with the disjunction elimination ∨ES The rule used for disjunction elimination is

Γ ⊢ A ∨ B Γ ⊢ A ⇒ C Γ ⊢ B ⇒ C ----------------------------------- [∨ES] Γ ⊢ C

Given a formula, the software builds a proof or an interpretation that falsifies it.

If the formula has an intuitionistic proof (without reduction ad absurdum), the software builds an intuitionistic proof

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

There are no rules for negation and for equivalence. The formula ¬A is considered an abreviation of A ⇒F and the formula A⇔B is considered an abreviation of (A ⇒ B) ∧ (B ⇒ A). - Propositional natural deduction with the disjunction elimination ∨E The rule used for disjunction elimination is

Γ ⊢ A ∨ B Γ, A ⊢ C Γ, B ⊢ C ----------------------------------- [∨E] Γ ⊢ CThis software works as the one above, the only difference is the rule used for disjonction elimination.

- 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.

- 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. The prover is complete : if the set of clauses is unsatisfiable and if there is no limit on time of proof and size of clauses, it will deduce the empty clause.
- Strategy "prover9" in first order logic We have two lists of clauses, one is the support list and the other is the usable list. From these two lists, the software tries to build a proof of the empty clause within the imposed limits. The prover is complete, that means, if the usable list is satisfiable and if the set of all clauses is unsatisfiable, and if there is no limit of time of proof and size of the clauses, it will deduce the empty clause.
- 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. The prover is complete : if the set of clauses is unsatisfiable and if there is no limit on time and length of proof, it will deduce the empty clause.