Déduction Naturelle

Une technique de calcul des preuves qui dérive des conclusions à partir d'hypothèses en appliquant des règles d'introduction et d'élimination pour chaque connecteur logique et quantificateur ; les preuves sont organisées en enchaînements d'applications de règles plutôt qu'en instanciations de schémas d'axiomes.