On présente des outils simples pour l'enseignement de la
logique.
Ces logiciels sont mis à la
disposition de tous, avec l'appui du laboratoire
VERIMAG.
Étant donnée une formule, le logiciel en construit une preuve ou
une interprétation
la falsifiant.
Étant donnée une formule et une preuve, le logiciel annote la preuve en
indiquant les règles appliquées
Étant donnée une formule, le logiciel traduit la formule dans S4
et soit constuit une preuve de sa traduction dans S4, soit fournit une
interprétation la falsifiant.