💻 computer science

Labelled Sequent Calculi for Propositional Team Logics

Cet article présente des calculs des séquents étiquetés son et complets avec des règles structurelles admissibles et des procédures de recherche de preuve terminantes pour quatre logiques d'équipes propositionnelles, incluant la logique inquisitive de base et la logique de dépendance intuitionniste propositionnelle, ainsi que leurs extensions par disjonction tensorielle.

Auteurs originaux : Fausto Barbero, Marianna Girlando, Valentin Müller, Fan Yang

Publié 2026-07-01

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Fausto Barbero, Marianna Girlando, Valentin Müller, Fan Yang

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de résoudre un casse-tête logique. De la manière traditionnelle (appelée « sémantique tarskienne »), vous abordez le casse-tête sous un seul et même angle. Vous demandez : « Cette affirmation est-elle vraie juste ici, en cet endroit précis ? »

Mais les auteurs de cet article travaillent avec un type de logique différent appelé Sémantique d'Équipe (Team Semantics). Au lieu de regarder un seul point, imaginez que vous regardez une équipe entière de personnes debout ensemble. Vous ne demandez pas si une affirmation est vraie pour une seule personne ; vous demandez si elle est vraie pour l'ensemble du groupe agissant de concert.

Cette approche par « équipe » est utilisée dans des scénarios du monde réel comme déterminer comment les variables dépendent les unes des autres dans une base de données (par exemple, « Est-ce que le prix dépend de la couleur ? ») ou comprendre le sens des questions dans le langage (par exemple, « Est-il vrai qu'il pleut OU est-il vrai qu'il neige ? »).

Le Problème : Comment prouver des choses sur les équipes

Les auteurs ont voulu créer un ensemble de règles (une « calculatrice ») pour prouver si des affirmations concernant ces équipes sont vraies ou fausses. Ils appellent cela des Calculs de Séquents Étiquetés (Labelled Sequent Calculi).

Considérez un « séquent » comme une balance à plateaux. D'un côté, vous avez une liste de faits que vous connaissez (l'état actuel de l'équipe). De l'autre côté, vous avez une conclusion que vous voulez prouver. Le but est de montrer que si les faits sur la gauche sont vrais, la conclusion sur la droite doit également être vraie.

L'article présente quatre « calculatrices » (systèmes de preuve) spécifiques pour quatre types différents de logique d'équipe :

Logique Inquisitive de Base : La logique d'équipe standard pour les questions.
Logique de Dépendance Intuitionniste Propositionnelle : Une logique d'équipe qui gère la « dépendance » (comme « A dépend de B »).
Deux versions étendues : Elles ajoutent une « Disjonction Tensorielle » spéciale (une façon sophistiquée de dire « diviser l'équipe en deux groupes distincts pour vérifier différentes choses »).

Les Outils : Les étiquettes comme membres d'équipe

Pour faire fonctionner ces calculs, les auteurs utilisent des étiquettes.

Imaginez que chaque membre de votre équipe porte un badge nominatif.
Certains badges sont pour des individus (des personnes seules).
D'autres sont pour des groupes (l'équipe entière).
Les règles permettent de dire des choses comme « Le groupe x est le même que le groupe y » ou « Le groupe x est un sous-ensemble du groupe y ».

L'article présente deux types principaux de ces calculs :

1. La Calculatrice « Détaillée » (G(L))

Cette version est très précise. Elle utilise des étiquettes complexes qui peuvent représenter des équipes, leurs unions (fusionner deux équipes) et leurs intersections (trouver le chevauchement entre deux équipes).

Analogie : C'est comme un GPS haut de gamme qui suit chaque voiture dans un embouteillage, leurs positions exactes, et comment elles fusionnent ou changent de voie. C'est mathématiquement rigoureux et reflète exactement comment les équipes se comportent dans le monde réel.
Le Piège : Parce qu'elle suit énormément de détails, il est difficile de dire si le GPS finira par arrêter de calculer (il pourrait tourner indéfiniment).

2. La Calculatrice « Terminante » (G*(L))

Pour résoudre ce problème de « calcul infini », les auteurs ont créé une version simplifiée.

Analogie : Au lieu de suivre le mouvement exact de chaque voiture, ce GPS dit simplement : « Nous avons une liste de 5 voitures. Vérifions toutes les combinaisons possibles de ces 5 voitures. »
L'Astuce : Ils supposent qu'il existe un nombre fini de « états » possibles (comme un nombre limité de conditions météorologiques possibles). Comme le nombre de possibilités est limité, la calculatrice est garantie de s'arrêter après un certain temps. Elle trouvera soit une preuve (Succès !) soit elle heurtera un mur où plus aucune règle ne s'applique (Échec/Contre-exemple).
Pourquoi c'est important : Cela garantit que vous pouvez toujours écrire un programme informatique pour décider si une affirmation est vraie ou fausse dans ces logiques.

Les Règles Clés du Jeu

L'article prouve que leurs calculs sont Sains (Sound) et Complets (Complete) :

Sain : Si la calculatrice dit « Vrai », c'est réellement Vrai. (La calculatrice ne ment pas).
Complet : Si quelque chose est réellement Vrai, la calculatrice peut finir par trouver une preuve pour cela. (La calculatrice ne manque rien).

Ils ont également prouvé que les calculs possèdent des règles admissibles.

Affaiblissement (Weakening) : Vous pouvez ajouter des faits supplémentaires et inutiles à votre liste sans briser la logique.
Contraction : Si vous listez le même fait deux fois, vous pouvez le traiter comme s'il n'était listé qu'une seule fois.
Coupure (Cut) : Si vous prouvez que A mène à B, et que B mène à C, vous pouvez passer directement de « A mène à C » sans montrer l'étape intermédiaire.

Le Défi du « Tensor »

L'une des parties les plus difficiles de cet article était de traiter la Disjonction Tensorielle (la règle de « division »).

L'Analogie : Imaginez une équipe de détectives.
- La logique standard dit : « Toute l'équipe résout l'affaire si tous sont d'accord sur la réponse. »
- La logique tensorielle dit : « L'équipe résout l'affaire si nous pouvons diviser les membres en deux groupes, où le Groupe A résout une partie de l'affaire et le Groupe B résout le reste. »
Les auteurs ont dû inventer une règle spéciale (appelée la règle fin) pour gérer cela. Parce qu'ils supposent que le nombre de « mondes » (valuations) est fini, ils ont pu dire : « Chaque équipe est simplement une combinaison de ces mondes spécifiques et limités. » Cela leur a permis de simuler mathématiquement le comportement de division.

Résumé

En bref, les auteurs ont construit deux ensembles de manuels de règles pour résoudre des casse-têtes logiques impliquant des groupes de personnes (équipes) :

Un manuel de règles détaillé et mathématiquement parfait qui gère les interactions de groupe complexes mais est difficile à automatiser.
Un manuel de règles simplifié et garanti de se terminer, qui suppose un nombre limité de possibilités, permettant aux ordinateurs de vérifier automatiquement si une affirmation est vraie ou fausse.

Ils ont prouvé que les deux manuels sont fiables (sains) et couvrent toutes les vérités (complets) pour les logiques spécifiques qu'ils ont étudiées.

Résumé Technique : Calculs Séquentiels Étiquetés pour les Logiques d'Équipe Propositionnelles

Énoncé du Problème
L'article traite des défis de la théorie de la démonstration associés aux logiques propositionnelles basées sur la sémantique d'équipe. Bien que les propriétés sémantiques des logiques d'équipe à clôture descendante (spécifiquement la logique inquisitive de base (InqB), la logique de dépendance intuitionniste propositionnelle (PID), et leurs extensions avec la disjonction tenseur (InqB $\lor$ et PID $\lor$ )) soient bien comprises, leur théorie de la démonstration demeure sous-développée. Les systèmes de preuve analytiques existants pour ces logiques, tels que les calculs de display multi-types ou les calculs séquentiels à inférence profonde, impliquent souvent des enrichissements structurels complexes de séquents de type Gentzen. Les auteurs identifient un besoin de calculs séquentiels étiquetés modulaires capables de gérer les conditions de satisfaction spécifiques de la sémantique d'équipe, particulièrement le comportement de la disjonction tenseur ( $\lor$ ) et des atomes de dépendance, tout en garantissant des propriétés telles que l'admissibilité de la coupure (cut-admissibility) et la terminaison de la recherche de preuve.

Méthodologie
Les auteurs développent deux familles de calculs séquentiels étiquetés pour les quatre logiques cibles :

Calculs Étiquetés Généraux ( $G(L)$ ) : Ces systèmes utilisent des étiquettes construites à partir d'ensembles infinis de variables de l'équipe ( $S$ pour les équipes singulières, $A$ pour les équipes arbitraires) combinées avec des opérations de théorie des ensembles (union $\cup$ et intersection $\cap$ ). Les étiquettes représentent des équipes arbitraires, des équipes singulières et leurs combinaisons. Les calculs incluent :
- Séquents Initiaux et Règles Logiques : Ils reflètent les conditions de satisfaction définies dans la sémantique d'équipe (par exemple, les règles pour $\land$ , $\lor$ , $\to$ , et le tenseur $\lor$ ).
- Règles d'Ordre : Un ensemble de règles formalisant les propriétés de la théorie des ensembles pour les équipes (par exemple, transitivité, union, intersection, et la propriété de l'équipe vide).
- Règles Spéciales : Une règle nommée fin est introduite pour traiter l'hypothèse selon laquelle l'ensemble des variables propositionnelles $P$ est fini. Cette règle permet au système de décrire toute équipe comme une union de $2^{|P|}$ évaluations, ce qui est crucial pour simuler la disjonction tenseur sur les formules classiques.
- Modularité : Les systèmes sont conçnés de telle sorte que les calculs pour PID et PID $\lor$ sont obtenus en ajoutant des règles spécifiques pour les atomes de dépendance aux calculs pour InqB et InqB $\lor$ .
Calculs Terminants ( $G^\star(L)$ ) : Pour faciliter la recherche de preuve automatisée, les auteurs introduisent une variante simplifiée où les étiquettes sont définies comme des ensembles finis de variables plutôt que comme des termes complexes impliquant des unions et des intersections. Cette approche élimine le besoin de règles atomiques relationnelles et de règles d'ordre, les remplaçant par des règles opérant directement sur l'ensemble des variables contenues dans une étiquette.

Contributions Clés et Résultats

Correction et Complétude : Les auteurs prouvent que les calculs généraux $G(L)$ sont corrects par rapport aux sémantiques d'équipe et aux axiomatisations de type Hilbert, ainsi que complets. Ceci est établi en démontrant l'admissibilité des règles structurelles (affaiblissement, contraction, coupure) et en établissant l'admissibilité des règles dérivées (telles que mp pour le modus ponens et flat pour la platitude des formules classiques).
Admissibilité de la Coupure : Un résultat technique central est la preuve de l'admissibilité de la coupure pour les quatre calculs. La preuve procède par induction sur le rang de la formule de coupure et la hauteur de la dérivation, utilisant un ordonnancement lexicographique qui prend en compte à la fois la complexité de la formule et l'étiquette.
Recherche de Preuve Terminante : L'article présente des algorithmes de recherche de preuve explicites et terminants pour les calculs simplifiés $G^\star(L)$ . L'algorithme construit une arborescence de recherche de preuve de manière ascendante (root-first). Il est prouvé qu'il termine car le nombre de formules étiquetées possibles est fini (étant donné un ensemble fini de variables propositionnelles et un ensemble fini de sous-formules).
Procédures de Décision : La nature terminante des calculs $G^\star(L)$ implique que les problèmes de satisfaisabilité et de validité pour InqB, PID, InqB $\lor$ et PID $\lor$ sont décidables. Les auteurs fournissent une construction de contre-modèle à partir de toute branche saturée (ouverte) de l'arborescence de recherche de preuve, garantissant la complétude de la procédure de recherche.

Signification et Revendications
L'article affirme que sa contribution principale réside dans la fourniture des premiers calculs séquentiels étiquetés corrects et complets couvrant toute la gamme des logiques d'équipe propositionnelles, incluant la disjonction tenseur et les atomes de dépendance. Les auteurs soulignent deux avantages distincts de leur approche :

Modularité : Les systèmes de preuve peuvent être adaptés à différents ensembles de connecteurs ou d'atomes en ajoutant ou en supprimant simplement des règles, une caractéristique absente des calculs structurés plus rigides trouvés dans la littérature précédente.
Terminaison et Décision : En simplifiant la structure des étiquettes dans $G^\star(L)$ , les auteurs fournissent une procédure de décision concrète pour ces logiques, une étape significative pour le raisonnement automatisé en sémantique d'équipe.

Les auteurs notent que bien que les calculs généraux $G(L)$ puissent produire des preuves plus courtes grâce aux règles à prémisse fixe et à la capacité de raisonner sur des sous-ensembles arbitraires via les variables, les calculs simplifiés $G^\star(L)$ sont essentiels pour établir la terminaison. Le travail est restreint aux langages possédant un nombre fini d'atomes propositionnels, une condition nécessaire pour la règle fin et la terminaison de la recherche de preuve en présence de la disjonction tenseur. L'article conclut en identifiant des travaux futurs, notamment l'extension de ces systèmes à des langages avec une infinité d'atomes et le développement de systèmes de preuve pour d'autres classes de logiques d'équipe, telles que celles sans implication intuitionniste ou celles possédant la propriété de clôture par union.