Résumé technique : Sur les notions d'équivalence forte en programmation logique et en argumentation abstraite

1. Énoncé du problème

L'article traite d'une divergence fondamentale entre la Programmation Logique (PL) et l'Argumentation Abstraite (AA) concernant l'équivalence forte. Bien que ces deux formalismes soient connus pour être sémantiquement équivalents dans des contextes statiques (où un programme logique $P$ peut être mappé vers un cadre d'argumentation $F$ de telle sorte que leurs solutions — ensembles de réponses et extensions stables — coïncident), cet alignement échoue dans des contextes dynamiques.

L'équivalence forte exige que deux bases de connaissances restent équivalentes sous toute mise à jour possible (expansion). Les auteurs démontrent que deux programmes logiques $P$ et $Q$ peuvent être fortement équivalents ($P \equiv_s Q$), alors que leurs cadres d'argumentation correspondants $F_P$ et $F_Q$ ne le sont pas ($F_P \not\equiv_s F_Q$).

Le Décalage Central :
La divergence provient de notions différentes de mise à jour :

• En Argumentation : Les mises à jour consistent à ajouter de nouveaux arguments et de nouvelles attaques. Un argument existant peut être attaqué par un nouveau, effaçant ainsi efficacement son statut.
• En Programmation Logique : Les mises à jour consistent généralement à ajouter de nouvelles règles. Les faits (règles à corps vide) ne peuvent pas être écrasés par de nouvelles informations ; ils persistent sauf s'ils sont explicitement contredits par la sémantique du modèle stable.
• Exemple : Dans un scénario où l'alibi d'un suspect est établi par un fait, l'ajout d'une nouvelle règle indiquant que l'alibi est faux (en raison d'un témoin) ne supprime pas le fait original dans les mises à jour standard de PL. En revanche, en AA, un nouvel argument attaquant l'argument de l'alibi supprimerait l'alibi de l'extension. Cela conduit à des résultats de raisonnement différents lorsque la même connaissance est mise à jour dans les deux formalismes.

2. Méthodologie

Les auteurs emploient une analyse syntaxique et sémantique des traductions entre les PL et les cadres d'argumentation, en se concentrant sur trois classes spécifiques :

1. Les PL atomiques strictes h-unic et les Cadres d'Argumentation (CA) stricts (de style Dung).
2. Les PL atomiques générales (autorisant la non-strictesse) et les CA stricts avec attaques non ancrées.
3. Les PL atomiques générales et les Cadres d'Argumentation à Revendications Bien Formés (CAFR).

Étapes techniques clés :

• Assouplissement de la strictesse : Les auteurs étendent les bijections existantes (par exemple, de [5]) pour gérer les programmes et cadres non stricts. Ils introduisent des attaques non ancrées (attaques provenant d'arguments en dehors de l'ensemble courant $A$) pour mapper les littéraux négatifs dans les PL qui n'apparaissent pas comme têtes de règles.
• Raffinement de Règle (RR) : Pour résoudre le décalage dynamique, les auteurs introduisent un nouvel opérateur de mise à jour pour les programmes logiques appelé Raffinement de Règle.
  • Au lieu d'ajouter simplement une nouvelle règle $r'$ à un programme $P$, le RR vérifie si une règle avec le même identifiant (ou la même tête, dans le cas h-unique) existe déjà.
  • Si elle existe, le corps de la règle existante est raffiné (fusionné) avec le corps de $r'$, plutôt que d'ajouter une règle concurrente. Cela imite le comportement de l'ajout d'une attaque à un argument existant en AA.
  • Deux opérateurs de mise à jour distincts sont définis :
    • Mise à jour $\uplus$ : Pour les programmes h-unique (identifiés par les atomes de tête).
    • Mise à jour $+ \sqcup$ : Pour les programmes atomiques généraux (identifiés par des IDs de règles explicites).
• Caractérisation par noyaux : Les auteurs adaptent le concept de noyaux (modifications syntaxiques utilisées pour caractériser l'équivalence forte en AA) aux programmes logiques. Ils définissent un noyau ASP où les vulnérabilités dispensables (littéraux négatifs correspondant à des boucles auto-attaquantes) sont supprimées.

3. Contributions clés

A. Équivalence statique étendue

L'article établit que l'équivalence sémantique vaut entre :

• Les PL atomiques strictes h-unique et les CA stricts.
• Les PL atomiques générales et les CA stricts (via des attaques non ancrées).
• Les PL atomiques générales et les CAFR bien formés.
  Crucialement, cette équivalence est préservée même lors de l'assouplissement de la contrainte de « strictesse », à condition que les attaques non ancrées soient prises en compte.

B. Le Raffinement de Règle comme solution

La contribution principale est la définition de l'Équivalence Forte sous Raffinement de Règle ($P \equiv_r Q$).

• Définition : Deux programmes sont fortement équivalents sous RR si, pour toute mise à jour $R$, le résultat du raffinement de $P$ avec $R$ produit les mêmes ensembles de réponses que le raffinement de $Q$ avec $R$.
• Mécanisme : Cet opérateur garantit que les mises à jour des PL se comportent structurellement comme les mises à jour des CA (ajout d'attaques/vulnérabilités) plutôt que comme de simples unions d'ensembles.

C. Théorèmes de caractérisation

Les auteurs prouvent que le Raffinement de Règle restaure l'alignement entre les deux formalismes :

1. Pour les programmes h-unique : $P \equiv_r Q$ si et seulement si $P$ et $Q$ ont le même noyau ASP. Cela équivaut à ce que leurs CA correspondants aient le même noyau stable et soient fortement équivalents au sens de l'AA.
2. Pour les programmes atomiques généraux : Une caractérisation syntaxique directe est fournie. Deux programmes sont RR-fortement équivalents si les corps de leurs règles coïncident (pour les IDs correspondants) et si leurs têtes coïncident (pour les règles non bouclantes).
3. Pour les CAFR : L'article définit une nouvelle notion d'équivalence forte pour les CAFR bien formés qui permet des mises à jour incompatibles (où les fonctions de revendication diffèrent) en priorisant la revendication originale. Cette nouvelle notion d'AA est prouvée équivalente à l'équivalence RR-forte dans les PL atomiques.

4. Résultats

• Proposition 10 : Confirme que l'équivalence forte standard dans les PL ($P \equiv_s Q$) n'implique pas l'équivalence forte dans leurs CA correspondants ($F_P \equiv_s F_Q$).
• Théorème 1 : Établit la chaîne d'équivalence pour les programmes h-unique :
  • $P$ et $Q$ ont le même noyau $\iff$ $F_P$ et $F_Q$ ont le même noyau stable $\iff$ $F_P \equiv_s F_Q$ $\iff$ $P \equiv_r Q$.
• Théorème 3 : Étend cette équivalence aux programmes atomiques généraux et aux CAFR bien formés, prouvant que $P \equiv_r^+ Q$ (équivalence RR-forte) est équivalente à $F_P \equiv_s F_Q$ (équivalence forte dans les CAFR sous la nouvelle définition de mise à jour).
• Corollaire 1 : Fournit une condition syntaxique concrète pour vérifier l'équivalence forte entre deux CAFR bien formés basée sur leurs ensembles d'arguments, leurs relations d'attaque et leurs fonctions de revendication.

5. Importance et affirmations

L'article prétend restaurer la compatibilité entre la Programmation Logique et l'Argumentation Abstraite dans des contextes dynamiques. En introduisant le Raffinement de Règle, les auteurs fournissent un cadre unifié où :

• L'équivalence forte est préservée à travers la traduction entre des classes spécifiques de PL et de CA/CAFR.
• Les « notions incongrues de mise à jour » sont réconciliées en alignant le mécanisme de mise à jour de la PL avec le mécanisme d'ajout d'attaques de l'AA.

Les auteurs positionnent leur travail comme une approche syntaxique qui traite directement le décalage, par opposition aux cadres sémantiques précédents (par exemple, [3]) qui tentent de combler le fossé via des modèles sémantiques généraux. Ils notent que si les modèles SE [16] caractérisent l'équivalence forte standard dans les PL, leur approche offre une caractérisation syntaxique directe (via les noyaux et le raffinement de règle) qui s'aligne sur les propriétés structurelles des cadres d'argumentation.

Limites et travaux futurs (tels que déclarés dans l'article) :

• Les résultats actuels s'appliquent aux programmes logiques atomiques. Les auteurs reconnaissent que l'extension de ceci à la classe complète des programmes logiques normaux (avec des dépendances positives dans le corps) reste un problème ouvert.
• Les travaux futurs consistent à relier le Raffinement de Règle aux opérateurs de révision de croyances en ASP et à explorer des caractérisations pour des CA plus expressifs, tels que les Cadres Dialectiques Abstraits (CDA).