Dans 5 secondes, vous serez redirigé vers une nouvelle version de cette page.
Veuillez mettre à jour
vos liens vers
http://membres-liglab.imag.fr/michel.levy/dn.php
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
Last modified: Wed Aug 3 11:50:16 CET 2005