Calcul des séquents | EPFL Graph Search

Ê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 GraphSearch.

Découvrez-en plus sur les applications Graph.

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.

À 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.

Concepts associés (66)

Cours associés (5)

Séances de cours associées (31)

MATH-381: Mathematical logic

Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

EE-431: Advanced VLSI design

In this project-based course, students collect hands-on experience with designing full-custom digital VLSI circuits in dynamic logic. They learn to carry out the design and optimization on transistor

Calcul des séquents

Logique

La logique — du grec , qui est un terme dérivé de signifiant à la fois « raison », « langage » et « raisonnement » — est, dans une première approche, l'étude de l'inférence, c'est-à-dire des règles formelles que doit respecter toute argumentation correcte. Le terme aurait été utilisé pour la première fois par Xénocrate. La logique antique se décompose d'abord en dialectique et rhétorique. Elle est depuis l'Antiquité l'une des grandes disciplines de la philosophie, avec l'éthique (philosophie morale) et la physique (science de la nature).

Théorie de la démonstration

La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du . Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au congrès international des mathématiciens en 1900 avec pour objectif de démontrer la cohérence des mathématiques.

Proposition : Démonstration par motif absurde MOOC: Analyse I

Examine la proposition selon laquelle X2 n'est pas égal à 2 en utilisant un raisonnement absurde.

Calcul séquentiel: bases et applications CS-550: Formal verification

Couvre les bases et les applications du calcul séquentiel en logique et théorie des preuves, y compris l'élimination des coupes et l'analyse des preuves pratiques.

Calcul des propositions

Couvre le calcul des propositions dans la logique de prédicat en mettant l'accent sur les connectifs logiques.