Une extension du calcul des sequents qui manipule des collections (multiensembles) de sequents — appelées hyperséquents — en parallèle, fournissant des mécanismes structurels pour capturer des logiques d'intermédiaire force et de nombreuses logiques non classiques en permettant la communication et l'interaction entre sequents composants.

Principe

Considérer l'état de preuve comme un hypersequent, c'est-à-dire une collection finie de sequents séparés par un délimiteur parallèle ; les règles opèrent soit à l'intérieur de sequents composant, soit entre composants (règles de communication), autorisant des dérivations reflétant des propriétés structurelles non classiques comme la prélinéarité ou certaines interactions modales/temporelles.

Démonstration

Pour capturer une logique satisfaisant la prélinéarité, une règle d'hypersequent peut permettre de déplacer une formule d'un sequent composant à un autre ou de combiner des composants pour décharger des hypothèses ; par exemple, prouver A→B∨B→A peut utiliser des sequents multiples en parallèle où le raisonnement par composant et une règle de communication donnent la tautologie souhaitée dans le calcul des hyperséquents.

Mauvaise application

Utiliser les hyperséquents comme de simples multisets de sequents sans mettre en œuvre les règles de communication ou structurelles prévues peut déformer la logique visée ; de même, ajouter des règles inter-composants non restreintes peut effondrer les distinctions entre logiques et produire des systèmes non valides par rapport à la sémantique originale.

Conséquence

Conçus pour une logique cible, les calculs d'hyperséquents capturent un éventail plus large de comportements structurels que les systèmes à sequent unique, fournissent souvent des systèmes sans coupure pour des logiques intermédiaires et modales, clarifient la recherche de preuve en parallèle et permettent des extensions modulaires en ajoutant des règles composants/communication.

Inversion

L'approche inverse est le calcul à sequent unique où un seul sequent est manipulé à la fois ; les calculs à sequent unique suffisent souvent pour la logique classique mais échouent à représenter certains principes non classiques que les hyperséquents modélisent naturellement via l'interaction des composants.

Limite

Les méthodes d'hyperséquents s'appliquent lorsque l'interaction parallèle des composants modélise la sémantique de la logique (logiques intermédiaires, certaines logiques modales et sous-structurelles) ; elles ne sont pas nécessaires pour les logiques déjà traitées par un sequent unique et exigent un dessin soigné des règles inter-composants pour éviter des extensions non valides ou trivialisantes.

Tension sémantique

Tension entre les hyperséquents et d'autres formalismes multi-structures (sequent labellés, sequents imbriqués, calculs d'affichage) : chaque formalisme expose une discipline différente pour l'interaction et la comptabilité inter-composants ; le choix implique des arbitrages en modularité, complexité de recherche de preuve et adéquation sémantique.

Synthèse

Le Calcul des Hyperséquents généralise les sequents en collections parallèles de sequents et dote la théorie de la preuve de règles agissant à l'intérieur et entre composants : en formalisant la communication inter-composants contrôlée, il capture les propriétés structurelles de nombreuses logiques non classiques et produit des systèmes modulaires, souvent sans coupure, adaptés à leur sémantique.