Déduction Naturelle

• Logiciel
Pour vous aider à faire des preuves , je propose deux prouveurs.
L'architecture web et les principes de ces prouveurs sont des adaptations du travail du Professeur Staerk assistant à l'ETH jusqu'en 2005.
• Le premier prouveur utilise librement la réduction à l'absurde, et les preuves obtenues sont courtes.
• Le deuxième prouveur utilise le théorème de Glivenko (1929) :
  la formule propositionnelle A est classiquement prouvable si et seulement si il y a une preuve intuitioniste de -- A
  Soit A la formule à prouver :
  s'il existe une preuve intuitioniste de A , le prouveur la donne, sinon il donne une preuve intuitutioniste de --A , suivie de la formule A obtenue par une seule application de la réduction à l'absurde.
  Le prouveur intuitioniste 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