Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Calcul des séquents
Résumé
En logique mathématique et plus précisément en théorie de la démonstration, le calcul des séquents est un système de déduction créé par Gerhard Gentzen. Le nom de ce formalisme fait référence à un style particulier de déduction ; le système original a été adapté à diverses logiques, telles que la logique classique, la logique intuitionniste et la logique linéaire. Un séquent est une suite d'hypothèses suivie d'une suite de conclusions, les deux suites étant usuellement séparées par le symbole (taquet droit), « : » (deux-points) ou encore (flèche droite) dans l'œuvre originale de Gentzen.
Un séquent représente une étape d'une démonstration, le calcul des séquents explicitant les opérations possibles sur ce séquent en vue d'obtenir une démonstration complète et correcte.
En 1934, Gentzen a proposé la déduction naturelle, un formalisme pour décrire les preuves du calcul des prédicats, dont l'idée était de coller au plus près à la manière dont les mathématiciens raisonnent. Il a ensuite tenté d'utiliser la déduction naturelle pour produire une preuve syntaxique de la cohérence de l'arithmétique, mais les difficultés techniques l'ont conduit à reformuler le formalisme en une version plus symétrique : le calcul des séquents. Contrairement à la déduction naturelle où un jugement est une suite d'hypothèses suivie d'une conclusion, dans le calcul des séquents, un jugement peut contenir plusieurs conclusions. C'est dans ce cadre qu'il a démontré ce qui devait devenir l'un des théorèmes principaux de la théorie de la démonstration : le théorème délimination des coupures. Dag Prawitz a montré en 1965 que ce théorème pouvait se transporter à la déduction naturelle.
Le terme calcul des séquents est une traduction de l'anglais sequent calculus, lui-même hérité de l'allemand Sequenzenkalkül.
L'objet de base du calcul est le séquent, qui est un couple de listes finies (éventuellement vides) de formules, séparées par un symbole qui se lit « thèse ». Les séquents sont ainsi usuellement notés :
où les sont les hypothèses et les sont les conclusions du séquent.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.