Déduction naturelle vs Calcul des séquents

[sunyata]

Bonjour,

Quelles différence y-at-il entre ce qu'on appelle "déduction naturelle" & "calcul des séquents" ?

Si j'ai bien compris les 2 méthodes visent à démontrer la validité d'une formule, mais dans la déduction naturelle, on manipule les formules
de manière à la simplifier autant que possible, alors que pour le calcul des séquents, on reconstruit l'arbre de démonstration jusqu'aux axiomes.

Cela vous semble-t-il correct ? Autre question : Peut-on combiner les 2 méthodes pour faciliter une démonstration ?

Cordialement
-----

[GBZM]

Bonsoir,

Je ne comprends pas ton paragraphe "Si je comprends bien...".

Une démonstration en déduction naturelle est un arbre, ou les noeuds sont des formules, avec en haut des hypothèses (dont certaines sont déchargées au cours de la démonstration) et en bas une formule démontrée sous les hypothèses non déchargées. Les règles de déduction sont de la forme introduction / élimination de connecteurs ou de quantificateurs.

Une démonstration en calcul des séquents est aussi un arbre, mais cette fois ci les noeuds sont des séquents de la forme où sont des listes finies de formules. Les règles de déduction sont des règles structurelles et des règles d'introduction à gauche ou à droite de de connecteurs ou de quantificateurs.

Les deux systèmes ont été formalisés par G. Gentzen. La forme plus symétrique du calcul des séquents lui a été plus commode pour certaines démonstrations.