Simple tools for teaching logic are presented.
These softwares are made available to all, with the support of the
Propositional natural deduction
Given a formula, the software builds a proof or an interpretation that falsifies it.
Given a formula and proof, the software annotates the proof by indicating the rules applied.
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.
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
or an interpretation that falsifies it.
Last change : 27-Apr-2019