Calcul des séquents
système de déduction mathématique / De Wikipedia, l'encyclopédie encyclopedia
Cher Wikiwand IA, Faisons court en répondant simplement à ces questions clés :
Pouvez-vous énumérer les principaux faits et statistiques sur Calcul des séquents?
Résumez cet article pour un enfant de 10 ans
« Séquent » redirige ici. Pour l’article homophone, voir 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 système de déduction créé par Gerhard Gentzen[1],[2],[3]. 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[4]), « : » (deux-points[5]) 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.