Voir la source de Calcul des séquents

{{redirect homophones|Séquent|Sécant}}
En [[logique mathématique]] et plus précisément en [[théorie de la démonstration]], le '''calcul des séquents''' est un [[logique mathématique#Systèmes de déduction|système de déduction]] créé par [[Gerhard Gentzen]]<ref>
{{Ouvrage
 | auteur1=Gerhard Gentzen
 | traducteur=R. Feys et J. Ladrière
 | titre=Recherches sur la déduction logique
 | titre original=Untersuchungen über das logische schließen
 | éditeur=Presses universitaires de France
 | année=1955
 }}{{Commentaire biblio|Traduit et commenté.}}</ref>{{,}}<ref name="SchließenI">
{{article
 | langue =
 | prénom1 = Gerhard
 | nom1 =  Gentzen
 | lien auteur1 = Gerhard Gentzen
 | titre =      Untersuchungen über das logische Schließen. I
 | périodique = Mathematische Zeitschrift
 | lien périodique =
 | volume = 39
 | numéro =
 | jour =
 | mois =
 | année =      1935
 | pages =176-210
 | ISSN =
 | lire en ligne = http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN002375508
 | commentaire = manuscrit reçu en 1933.
}}</ref>{{,}}<ref>
{{article
 | langue =
 | prénom1 = Gerhard
 | nom1 =  Gentzen
 | lien auteur1 = Gerhard Gentzen
 | titre =      Untersuchungen über das logische Schließen. II
 | périodique = Mathematische Zeitschrift
 | lien périodique =
 | volume = 39
 | numéro =
 | jour =
 | mois =
 | année =      1935
 | pages =405–431
 | ISSN =
 | url texte =
 | consulté le =
 |  doi = 10.1007/BF01201363
 | commentaire = manuscrit reçu en 1933.
}}</ref>. 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 <math>\vdash</math> (taquet droit<ref>{{pdf}} Table unicode des [https://www.unicode.org/fr/charts/PDF/Unicode-3.2/U32-2200.pdf opérateurs mathématiques].</ref>), « : » (deux-points<ref>{{Ouvrage|langue=fr|auteur1=R. Lalement|titre=Logique, réduction, résolution|éditeur=Masson|année=1990|passage=p. 129|isbn=}}.</ref>) ou encore <math>\rightarrow</math> (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.

== Historique et motivation ==

En 1934<ref name="SchließenI"/>, 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|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<ref>{{Ouvrage|langue=en|prénom1=Dag|nom1=Prawitz|titre=Natural deduction|sous-titre=A proof-theoretical study|éditeur=Almqvist & Wicksell|collection=Acta Universitatis Stockholmiensis, Stockholm studies in philosophy 3|lieu=Stockholm, Göteborg, Uppsala|année=1965}}.</ref>.

Le terme ''calcul des séquents'' est une traduction de l'anglais ''sequent calculus'', lui-même hérité de l'allemand ''Sequenzenkalkül''<ref>La traduction littérale de l'allemand en français donnerait plutôt ''calcul des séquences''.</ref>.

== Définition ==

=== Séquent ===

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 :
<center>
<math>A_1,\dots, A_n\vdash B_1,\dots, B_p</math>
</center>
où les <math>A_i</math> sont les ''hypothèses'' (ou ''antécédents'') et les <math>B_j</math> sont les ''conclusions'' (ou ''conséquents'', ou ''succédents'') du séquent. Un autre point important à noter est qu'une même formule peut apparaître plusieurs fois à gauche et/ou à droite dans un séquent, par exemple <math>A_1</math> peut être la même formule que <math>A_n</math> ; on dit alors que cette formule a plusieurs ''occurrences'' dans le séquent.

==== Interprétation d'un séquent ====

La notation ''séquent'' peut se comprendre comme une astuce syntaxique pour dénoter des formules particulières ; la virgule à gauche s'interprète comme une [[Conjonction logique|conjonction]], la virgule à droite comme une [[Disjonction logique|disjonction]] et le symbole <math>\vdash </math> comme une [[Implication (logique)|implication]], si bien que le séquent ci-dessus peut se comprendre comme une notation pour la formule :
<center>
<math>(A_1\land \dots\land A_n )\rightarrow (B_1\lor \dots\lor B_p)</math>
</center>
et se lit ''intuitivement'' :

<center>
<math>A_1</math> et... et <math>A_n</math> impliquent <math>B_1</math> ou... ou <math>B_p</math>
</center>

mais le sens précis de ces symboles n'est donné que par les règles formelles (axiomes) qui suivent.

Lorsque la liste d'hypothèses est vide, on peut l'interpréter comme le vrai (c'est-à-dire l'élément neutre de la conjonction) et lorsque la liste de conclusions est vide, on peut l'interpréter comme le faux (c'est-à-dire l'élément neutre de la disjonction).

=== Règles ===
Une règle d'un calcul de séquent est de la forme :
<math>
 \cfrac{\textrm{premisses}}
       {\textrm{conclusion}}
</math>. On note à droite le nom de la règle.

Des règles du calcul des séquents spécifient comment à partir d'un certain nombre (éventuellement nul) de séquents ''prémisses'', on peut dériver un nouveau séquent ''conclusion''.

Une des propriétés importante du calcul des séquents est la ''réversibilité'' (ou ''inversibilité'') de certaines [[Règle d'inférence|règles d'inférence]], ce qui signifie l'''équivalence logique'' entre les prémisses et les conclusions (voir plus bas pour le système LK de la logique classique du premier ordre) <ref name=":0">{{Lien web |auteur=Olivier Laurent |titre=Théorie de la démonstration (ENS Lyon) |url=https://perso.ens-lyon.fr/olivier.laurent/thdem11.pdf |format=pdf |date=2012 |page=19}}</ref>. On peut prouver cette équivalence en utilisant la section ''Interprétation d'un séquent'' ci-dessus.

== Le système LK ==
Gentzen<ref name="SchließenI" /> a introduit le système LK (pour “'''k'''lassische Prädikaten'''l'''ogik”) qui formalise la [[logique classique]] du premier ordre. On en donne ici une version légèrement modernisée{{Par qui}}{{Référence nécessaire|date=7 janvier 2018}}. La définition ci-dessous suppose un minimum de familiarité avec le [[calcul des prédicats]]. Dans chacune des règles les [[Alphabet grec|lettres grecques]] Gamma, Delta, etc. dénotent des suites de formules que l'on nomme des ''contextes'' : il s'agit de formules qui sont présentes dans la conclusion mais qui n'y sont pas ''introduites''<ref name=":1">{{Lien web |langue=en |auteur=Dale Miller (Inria, Ecole Polytechnique) |titre=Proof theory, proof search, and logic programming |url=http://www.lix.polytechnique.fr/~dale/mpri/ln2022-v1.pdf |format=pdf |date=2022 |page=27}}</ref>. On fait figurer les séquents prémisses au-dessus, séparés par un trait horizontal du séquent conclusion. Les règles d'inférence se divisent en trois groupes : le groupe ''identité'', le groupe ''structurel'' et le groupe ''logique'' (qui seront présentés dans les sections suivantes).

Il est important de noter que pour la plupart des règles (groupe logique et groupe identité), il existe deux types de formulation :

* Une formulation '''multiplicative''' ne fait apparaître les ''contextes'' de la conclusion qu’une seule fois par prémisse (et toujours du même côté du symbole « thèse »). De plus, toutes les sous-formules de la conclusion se retrouvent dans les prémisses (exception : la ''règle de coupure'', qui possède néanmoins bien une forme multiplicative et une forme additive, formées d'après l'applicabilité ou non du critère précédent sur les contextes)
* Une formulation est '''additive''' si une formule ''contexte'' de la conclusion apparaît plusieurs fois dans les prémisses, ou si une sous-formule ou une formule ''contexte'' apparaît dans la conclusion alors qu’elle n’apparaît pas dans les prémisses.

Cette distinction est très importante en pratique pour les algorithmes de recherche de preuves ou de construction de preuves<ref name=":1" />.

=== Groupe identité ===
Il est constitué de deux règles :
{|class="wikitable centre"
|-
|
<math>\cfrac{\qquad }{ A \vdash A} \quad \textrm{axiome}</math>
|
<math>\cfrac{\Gamma \vdash A, \Delta \qquad \Gamma', A \vdash \Delta'} {\Gamma, \Gamma' \vdash \Delta, \Delta'} \quad \textrm{coupure}</math>
|}
Une discussion sur la [[règle de coupure]] figure plus bas. Remarquons que la règle axiome est la seule de tout le calcul qui n'a pas de prémisse.

Pour les groupes structurel et logique, les règles viennent par paire selon le côté, gauche ou droit, du séquent où elles agissent.

La règle de coupure n'est pas ''réversible'' au sens défini plus haut. Elle est ici présentée ici sous sa forme ''multiplicative'' mais est irréversible y compris sous sa forme additive (on le perçoit intuitivement, dans la mesure où la formule ''A'' présente dans les deux séquents prémisses est absente de la conclusion).

=== Groupe structurel ===
Il est constitué de six règles :
{|class="wikitable centre"
|-
|
<math>
\cfrac
{\Gamma \vdash \Delta}
{ \Gamma,A \vdash \Delta} 
\quad \mathrm{affaiblissement\ gauche}
</math>
|
<math>
\cfrac
{\Gamma \vdash \Delta}
{\Gamma \vdash A,\Delta } 
\quad \mathrm{affaiblissement\ droite}
</math>
|-
|
<math>
\cfrac
{\Gamma,A,A \vdash \Delta}
{ \Gamma,A \vdash \Delta} 
\quad \mathrm{contraction\ gauche}
</math>
|
<math>
\cfrac
{\Gamma \vdash A,A,\Delta}
{\Gamma \vdash A,\Delta} 
\quad \mathrm{contraction\ droite}
</math>
|-
|
<math>
\cfrac
{\Gamma \vdash \Delta}
{ \sigma(\Gamma) \vdash \Delta} 
\quad \mathrm{\acute echange\ gauche}
</math>
|
<math>
\cfrac
{\Gamma \vdash \Delta}
{\Gamma \vdash \sigma(\Delta)} 
\quad \mathrm{\acute echange\ droite}
</math>
|}

Dans les règles d'échange la notation <math>\sigma(\Gamma)</math> désigne une permutation des (occurrences de) formules figurant dans <math>\Gamma</math>. Les règles d'échanges sont responsables de la [[commutativité]] de la logique. Par exemple, avec <math>\Gamma = A_1, A_2</math>, on pourra avoir <math>\sigma(\Gamma) = A_2, A_1</math>.

Les règles de contraction et d'affaiblissement expriment une forme d'[[idempotence]] des opérateurs « <math>\scriptstyle \lor</math> » et « <math>\scriptstyle \land</math> » de la logique : une formule <math>A</math> est équivalente aux formules <math>\scriptstyle A \lor A </math> et <math>\scriptstyle A \land A</math>.

Les règles d'affaiblissement ne sont pas ''réversibles'' au sens défini plus haut.

=== Groupe logique ===
Il est constitué de 12 règles :
{| class="wikitable centre"
|-
|
<math>
\cfrac
{\Gamma \vdash A,\Delta}
{ \Gamma,\lnot A \vdash \Delta} 
\quad \lnot\mathrm{ gauche}
</math>
|
<math>
\cfrac
{\Gamma,A \vdash \Delta}
{\Gamma \vdash \lnot A, \Delta } 
\quad \lnot\mathrm{ droite}
</math>
|-
|<math>
\cfrac
{\Gamma,A,B \vdash \Delta}
{ \Gamma,A\land B \vdash \Delta} 
\quad \land\mathrm{ gauche}
</math>
|
<math>
\cfrac
{\Gamma \vdash A,\Delta    \quad    \Gamma \vdash B,\Delta}
{\Gamma \vdash A\land B,\Delta } 
\quad \land\mathrm{ droite}
</math>
|-
|
<math>
\cfrac
{\Gamma,A \vdash \Delta    \quad     \Gamma,B \vdash \Delta}
{ \Gamma,A\lor B \vdash \Delta} 
\quad \lor\mathrm{ gauche}
</math>
|
<math>
\cfrac
{\Gamma \vdash A,B,\Delta}
{\Gamma \vdash A\lor B,\Delta } 
\quad \lor\mathrm{ droite}
</math>
|-
|
<math>
\cfrac
{\Gamma \vdash A,\Delta    \quad    \Gamma,B \vdash \Delta}
{ \Gamma,A\to B \vdash \Delta} 
\quad \to\mathrm{ gauche}
</math>
|
<math>
\cfrac
{\Gamma,A \vdash B,\Delta}
{\Gamma \vdash A\to B,\Delta } 
\quad \to\mathrm{ droite}
</math>
|-
|
<math>
\cfrac
{\Gamma,A[t/x] \vdash \Delta}
{ \Gamma,\forall x\cdot A \vdash \Delta} 
\quad \forall\mathrm{ gauche}
</math>
|
<math>
\cfrac
{\Gamma \vdash A,\Delta}
{\Gamma \vdash \forall x\cdot A,\Delta } 
\quad \forall\mathrm{ droite}
</math>
|-
|
<math>
\cfrac
{\Gamma,A \vdash \Delta}
{ \Gamma,\exists x\cdot A \vdash \Delta} 
\quad \exists\mathrm{ gauche}
</math>
|
<math>
\cfrac
{\Gamma \vdash A[t/x],\Delta}
{\Gamma \vdash \exists x\cdot A,\Delta } 
\quad \exists\mathrm{ droite}
</math>
|}

Les règles de quantificateurs sont soumises à des restrictions : dans les règles de <math>\forall</math>-droite et <math>\exists</math>-gauche, on demande que la variable <math>x</math> n'ait pas d'occurrence [[Variable libre|libre]] dans une des formules de <math>\Gamma</math> et <math>\Delta</math>.

La notation <math>A[t/x]</math> désigne la formule <math>A</math> dans laquelle la variable <math>x</math> est remplacée par un terme <math>t</math>, toutefois ce remplacement doit être ''sain'' : <math>A</math> ne doit pas contenir de sous-formule <math>\forall y.B</math> ou <math>\exists y.B</math> où <math>y</math> serait une variable libre de <math>B</math> apparaissant dans le terme <math>t</math>. Par exemple, <math>[y/x]</math> n'est pas une substitution saine dans <math>\forall z\exists y.P(x,y,z)</math> car après remplacement de <math>x</math> par <math>y</math>, on obtient : <math>\forall z\exists y.P(y,y,z)</math>, une variable (ici <math>y</math>) du terme remplaçant <math>x</math> s'est fait ''capturer'' par le quantificateur <math>\exists y</math>.

Les règles <math>\exists</math>droite et <math>
\forall 
</math>gauche ainsi définies ne sont pas ''réversibles'' <ref>{{Lien web |langue=en |auteur=Chung Liang |auteur2=Dale Miller |titre=Focusing Gentzen's LK proof system |url=http://www.lix.polytechnique.fr/~dale/papers/lkf-2020-04-03.pdf |format=pdf |site=lix.polytechnique.fr |date=2021 |page=6}}</ref>. Pour les autres règles, elles sont réversibles dans la présentation qui en est donnée ici (qui est un mélange de règles ''multiplicatives'' et ''additives''), mais elles ne le sont pas ''en toute généralité'', en particulier si l'on choisit de n'adopter que des règles additives ou que des règles multiplicatives<ref name=":0" />.  

=== Démonstrations ===

Une démonstration de LK est un arbre de séquents construit au moyen des règles ci-dessus de façon que chaque séquent soit conclusion d'exactement une règle ; la démonstration est terminée si l'on arrive à ce que toutes les feuilles de l'arbre soient des règles axiome. Le séquent racine de l'arbre est la conclusion de la démonstration. Voici un exemple de démonstration du principe de [[Proposition contraposée|contraposition]] de l'implication ; pour simplifier on a omis les utilisations de règles d'échange et représenté en gras les (occurrences de) formules dans les séquents prémisses sur lesquelles porte chaque règle :

<center>
[[Image:LK_dem_contraposition.png]]
</center>

== Théorème d'élimination des coupures ==
{{Article détaillé|Théorème d'élimination des coupures|règle de coupure}}
Aussi connu sous le nom de « théorème de Gentzen » ou « ''{{Lang|de|Hauptsatz}}'' » (parce que c'était le théorème principal des deux articles fondateurs de Gentzen), ce théorème énonce que toute démonstration en calcul des séquents peut être transformée en une démonstration de même conclusion, mais qui n'utilise pas la [[Règle de coupure|règle de la coupure]]. La démonstration de Gentzen fournit un algorithme qui, appliqué à une démonstration quelconque, aboutit à une démonstration sans coupures du même séquent conclusion. [[Helena Rasiowa]] et [[Roman Sikorski]] ont publié en 1959 une preuve sémantique du théorème de Gentzen pour le cas [[Logique classique|classique]], qui montre l'existence de la démonstration sans coupures, mais ne donne pas un procédé (de normalisation) qui y conduit étape par étape.

== Discussion ==

=== Le calcul des séquents et les autres formalismes logiques ===

Le calcul des séquents, contrairement aux [[systèmes à la Hilbert]] ou à la [[déduction naturelle]], n'a pas été créé pour être un formalisme intuitif qui refléterait une forme naturelle de raisonnement, car le propos de Gentzen était de résoudre certains problèmes techniques liés au fait que la [[Déduction naturelle#Réduction à l'absurde|règle de réduction à l'absurde]] brisait la symétrie intro/élim de la déduction naturelle. C'est pourquoi le calcul des séquents doit se penser comme un formalisme pour ''raisonner'' sur les preuves formelles plutôt que pour ''rédiger'' des preuves formelles. On peut toutefois facilement montrer que le calcul des séquents est équivalent à la déduction naturelle, au sens où les preuves formelles de l'un des formalismes se traduisent dans l'autre, et réciproquement<ref>Voir par exemple ''Proof and Types'', Jean-Yves Girard, Yves Lafont et Paul Taylor, Cambridge University Press, 1989</ref>.

L'intérêt du calcul des séquents est de rendre explicite un grand nombre de propriétés de la logique :

* la dualité hypothèse/conclusion exprimée par la symétrie parfaite entre la droite et la gauche dans les séquents ;
* la symétrie de la logique classique exprimée par le partitionnement des règles en gauche et droite ;
* les propriétés structurelles (commutativité, idempotence) exprimées par les règles du groupe structurel.

=== La règle de coupure ===
{{Article détaillé|règle de coupure}}
La [[règle de coupure]] est une généralisation du [[Modus ponens|''modus-ponens'']]. Pour le voir il faut considérer le cas particulier de la règle où :
* <math>\Gamma</math>, <math>\Delta</math> et <math>\Gamma'</math> sont des séquences vides de formules ;
* <math>\Delta'</math> contient une unique formule <math>B</math>.

Dans ce cas particulier les deux séquents prémisses de la règle deviennent respectivement <math>\vdash A</math> et <math>A\vdash B</math> tandis que le séquent conclusion devient <math>\vdash B</math>.

La règle de coupure joue un rôle très particulier dans le calcul des séquents pour deux raisons :

* elle est presque incontournable pour formaliser les démonstrations mathématiques ; en effet l'expérience montre que, à l'exception des démonstrations faciles de tautologies, la moindre démonstration de mathématique utilise très souvent la règle de coupure ;
* plus techniquement, c'est la seule règle à violer la ''propriété de la sous-formule'' ; si on observe les règles du calcul des séquents on voit que pour chaque règle, sauf la coupure, les formules apparaissant dans les séquents prémisses sont encore présentes dans le séquent conclusion. Autrement dit, si une démonstration du calcul des séquents n'utilise pas la règle de coupure, alors toutes les formules qu'elle contient sont des sous-formules du séquent conclusion, c’est-à-dire que le séquent conclusion de la démonstration est le plus compliqué de toute la démonstration.

La propriété de la sous-formule était très importante pour Gentzen car c'est elle qui permet de démontrer la cohérence du calcul. On peut en effet montrer que si le calcul mène à une contradiction, c'est-à-dire si l'on peut aussi bien prouver <math>\vdash A</math> que <math>\vdash \neg A</math>, alors on peut, moyennant la règle de coupure, prouver le séquent vide <math>\vdash</math> : il suffit d'utiliser la règle de négation

<math>
\cfrac
{\vdash \neg A}
{ \neg \neg A \vdash } 
</math>

puis la coupure

<math>
\cfrac
{\vdash \neg \neg A    \quad   \neg \neg A \vdash }
{ \vdash } 
</math>

Ainsi, toute contradiction mène au séquent vide. On en déduit, par simple contraposition, que si le séquent vide n'est pas prouvable, c'est qu'il n'y a pas de contradiction.

Par ailleurs, il est évident que le séquent vide n'a pas de sous-formule... précisément parce qu'il est vide ! Donc aucune règle satisfaisant la propriété de la sous-formule (selon laquelle le séquent conclusion contient toutes les formules des séquents prémisses) ne peut se conclure par le séquent vide. Dans la mesure où toutes les règles satisfont cette propriété à l'exception de la coupure, on en déduit que si l'on peut démontrer le séquent vide, ce ne peut être qu'à partir de la règle de coupure.

Or [[théorème de Gentzen|l'élimination des coupures]] montre précisément que la règle de coupure n'est jamais nécessaire : on peut toujours remplacer une démonstration avec coupure par une démonstration sans coupure<ref>Ce replacement a cependant le défaut qu'il remplace une démonstration courte par une démonstration longue et même très longue !</ref>. D'après ce qui précède, cela signifie en particulier que le séquent vide n'est pas démontrable, et plus généralement que le calcul des séquents ne contient aucune contradiction.

C'est en adaptant cette démonstration d'élimination des coupures au cas de l'arithmétique que [[Gerhard Gentzen|Gentzen]] a produit sa preuve de cohérence de l'arithmétique en utilisant un [[Récurrence transfinie|principe d'induction]] jusqu'à l'ordinal dénombrable [[nombre ordinal#Forme normale de Cantor|ε<sub>0</sub>]]<ref> Ce qui ne donne pas une preuve dans l'arithmétique de la cohérence de l'[[Axiomes de Peano|arithmétique]], car cette théorie, si elle est cohérente ne peut être démontrée telle dans l'arithmétique en vertu des [[théorèmes d'incomplétude de Gödel]].</ref>.

=== Logiques non-classiques ===
On obtient un système de preuve pour la [[logique intuitionniste]] à partir du système de preuve classique mais en restreignant les séquents à n'avoir qu'au plus une conclusion<ref>{{Lien web|titre=Proofs and types|auteur=[[Jean-Yves Girard|J.-Y. Girard]], Y. Lafond, P. Taylor|éditeur=Cambridge University Press|année=1989|page=38|isbn=0-521-37181-3|langue=en|url=www.paultaylor.eu/stable/prot.pdf}}</reF>. Ce nouveau système s'appelle LJ. De même il existe un calcul des séquents pour la [[logique linéaire]], appelé LL<ref>{{Lien web|titre=Proofs and types|auteur=[[Jean-Yves Girard|J.-Y. Girard]], Y. Lafond, P. Taylor|éditeur=Cambridge University Press|année=1989|page=159|isbn=0-521-37181-3|langue=en|url=www.paultaylor.eu/stable/prot.pdf}}</reF>.

== Implémentation ==
Le logiciel [[KeY (logiciel)|KeY]] (un outil de vérification formelle de programmes [[Java (langage)|Java]]) utilise le calcul des séquents<ref>{{Ouvrage|prénom1=Bernhard|nom1=Beckert|prénom2=Reiner|nom2=Hähnle|prénom3=Peter H.|nom3=Schmitt|titre=Verification of Object-oriented Software|sous-titre=The KeY Approach|éditeur=Springer-Verlag|année=2007|pages totales=658|isbn=978-3-540-68977-5|isbn2=3-540-68977-X|lire en ligne=https://dl.acm.org/citation.cfm?id=1808999|consulté le=2018-01-10}}</ref>.

== Notes et références ==
<references/>
== Voir aussi ==
* [[Logiques sous structurelles]]
* [[Antécédent (logique)]]
* [[Conséquent (logique)]]

== Liens externes ==
* [http://logitext.mit.edu/tutorial Un tutoriel pour apprendre le calcul des séquents]

== Bibliographie ==
* [[Jean-Yves Girard]], Yves Lafont et Paul Taylor, ''Proof and types'', [[Cambridge University Press]], 1989
* [[Jean-Yves Girard]], ''Le Point aveugle'', Tome I, chapitre 3 : « Les séquents classiques : LK », pp. 45-74. Éd. Hermann, mai 2006
* René David, Karim Nour, Christophe Raffali, ''Introduction à la logique, théorie de la démonstration'' 2001, [[Éditions Dunod|Dunod]], {{ISBN|2100067966}}, ''chap. 5''

{{Portail|mathématiques|logique|Informatique}}

[[Catégorie:Logique mathématique]]
[[Catégorie:Logique]]
[[Catégorie:Raisonnement mathématique]]
[[Catégorie:Méthode de démonstration]]
[[Catégorie:Théorie de la démonstration]]