Déduction Naturelle

• Logiciel
Pour vous aider à faire des preuves en déduction naturelle , je vous propose d'utiliser ce PROUVEUR.
L'architecture web et les principes de ce prouveur sont des adaptations du travail du Professeur Staerk assistant à l'ETH jusqu'en 2005. Considérons une formule propositionnelle.
Si la formule est intuitionistiquement prouvable, le prouveur en donne une preuve intuitioniste, c'est-à-dire sans réduction à l'absurde.
Si la formule est valide mais n'est pas intuitionistiquement prouvable, le prouveur en donne une preuve (utilisant des réductions à l'absurde).
Si la formule n'est pas valide, le prouveur en donne un contre-modèle.
La recherche des preuves intuitionistes est basé sur le système LJT décrit dans :
R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, J. Symb. Logic 57, pp 795--807, 1992. (ISSN 0022-4812)



• Documents
On recommande de consulter une histoire de déduction naturelle et de son enseignement écrite par Francis Jeffry Pelletier