Argumentation Abstraite : Grounded Extension - Pont Python/Tweety <=> Lean

Navigation : <- Tweety-11-Causal | Index

---

Objectifs pedagogiques

1. Calculer la grounded extension d’un cadre de Dung via deux implementations distinctes (Python naif et TweetyProject Java via jpype1), et demontrer leur equivalence sur un corpus de cadres de reference.
2. Relier la convergence numerique de l’iteration de la fonction caracteristique F au resultat formel Knaster-Tarski du lake argumentation_lean/.
3. Identifier le piege classique d’une implementation naive non monotone, et expliquer pourquoi la garantie du lake l’exclut (la definition mathematique du grounded est un point fixe de F, pas de sa variante incorrecte).

Prerequis

• jpype1 (pont JVM<->Python)
• TweetyProject 1.30 JARs (chargeables depuis libs/)
• Lean 4 (optionnel, pour lake build du companion)

Note de parite cross-langage. Ce notebook est un pont pedagogique entre l’implementation TweetyProject Java certifiee (utilisee comme oracle de reference) et le lake Lean 4 argumentation_lean/ qui formalise la meme theorie. Le notebook Tweety-5b-Lean-Argumentation.ipynb (deja en repo) execute la partie Lean en kernel lean4-wsl. Ce notebook-ci utilise uniquement Python+jpype1 pour rester executable sur toute machine qui a les JARs et le JDK portable.

Verdict SOTA. La lib noyau utilisee est TweetyProject 1.30 (paquet org.tweetyproject.arg.dung) - c’est la lib de reference canonique de la communaute argumentation. Aucun workaround degrade : on interroge directement SimpleGroundedReasoner qui implemente l’algo de Dung 1995. Axes 1-6 (sota-not-workaround.md) : (1) binding .NET natif IKVM aurait exige un wrapping .NET -> JAR via IKVM, hors-scope ; (2) P/Invoke N/A (Tweety = Java) ; (3) CLI Process.Start N/A (lib JVM, pas binaire externe) ; (4) IKVM pont Java : les JARs sont deja en JVM, pas besoin de pont ; (5) PythonNet : N/A car jpype1 est deja le pont Python-JVM canonique ; (6) lib differente a role equivalent : aucune lib Python n’implemente les 6+ semantiques de Dung avec le meme niveau de certification que Tweety. Verdict final = SOTA-OK.

Initialisation JVM Tweety + Outils Externes

Cette cellule suit le pattern du notebook Tweety-5 (deja merge) pour demarrer la JVM et charger les JARs. Le pattern tweety_init.py exige un cwd == Argument_Analysis/, donc on inline la detection (identique au notebook fonctionnel).

import os, pathlib, sys
import jpype
import jpype.imports

LIB_DIR = pathlib.Path("libs")
if not LIB_DIR.exists():
    LIB_DIR = pathlib.Path("../Argument_Analysis/libs")
if not LIB_DIR.exists():
    LIB_DIR = pathlib.Path("../../Argument_Analysis/libs")
if not LIB_DIR.exists():
    LIB_DIR = pathlib.Path("../../../Argument_Analysis/libs")

if not LIB_DIR.exists():
    print("ERREUR: dossier libs introuvable. Lancez d'abord:")
    print("  python download_tweety_tools.py --lib-dir")
    raise SystemExit(1)

jdk_portable = None
for jdk_path in [pathlib.Path("jdk-17-portable"),
                 pathlib.Path("../Argument_Analysis/jdk-17-portable"),
                 pathlib.Path("../../Argument_Analysis/jdk-17-portable")]:
    if jdk_path.exists():
        zulu_dirs = list(jdk_path.glob("zulu*"))
        if zulu_dirs:
            jdk_portable = zulu_dirs[0]
            os.environ["JAVA_HOME"] = str(jdk_portable.resolve())
            break

if jdk_portable is None:
    print("ERREUR: JDK portable introuvable.")
    raise SystemExit(1)

native_dir = LIB_DIR / "native"
classpath_items = []
if native_dir.exists():
    classpath_items.append(str(native_dir.resolve()))

jar_files = sorted(LIB_DIR.glob("*.jar"))
if not jar_files:
    print(f"ERREUR: aucun JAR dans {LIB_DIR}/")
    raise SystemExit(1)

classpath_items.extend(str(j.resolve()) for j in jar_files)
classpath = os.pathsep.join(classpath_items)

jvm_args = []
if native_dir.exists():
    jvm_args.append(f"-Djava.library.path={native_dir.resolve()}")

if jpype.isJVMStarted():
    print("JVM deja en cours d execution (reutilisation).")
else:
    jpype.startJVM(*jvm_args, classpath=[classpath])
    print(f"JVM demarree avec {len(jar_files)} JARs (JDK {jdk_portable.name}).")

print("--- Pret ---")
print(f"  JAVA_HOME = {os.environ.get('JAVA_HOME')}")
print(f"  JARs      = {len(jar_files)}")
print(f"  Native    = {native_dir.exists()}")

JVM demarree avec 41 JARs (JDK zulu17.50.19-ca-jdk17.0.11-win_x64).
--- Pret ---
  JAVA_HOME = C:\dev\CoursIA-tweety12\MyIA.AI.Notebooks\SymbolicAI\Argument_Analysis\jdk-17-portable\zulu17.50.19-ca-jdk17.0.11-win_x64
  JARs      = 41
  Native    = False

Verification des imports Dung

On importe les classes Java de TweetyProject pour la theorie de Dung : - DungTheory, Argument, Attack - la structure du cadre. - SimpleGroundedReasoner - l’implementation certifiee de la grounded extension, fondee sur l’algo de Dung (1995).

from org.tweetyproject.arg.dung.syntax import DungTheory, Argument, Attack
from org.tweetyproject.arg.dung.reasoner import (
    SimpleGroundedReasoner,
    SimpleStableReasoner,
    SimplePreferredReasoner,
    SimpleCompleteReasoner,
    SimpleAdmissibleReasoner,
    SimpleConflictFreeReasoner,
)
print("Imports Dung reussis.")

def construire_af(noms, attaques):
    af = DungTheory()
    args = {nom: Argument(nom) for nom in noms}
    for arg in args.values():
        af.add(arg)
    for src, tgt in attaques:
        af.add(Attack(args[src], args[tgt]))
    return af, args

def noms_extension(ext):
    return sorted([str(a.getName()) for a in ext])

print("Utilitaires prets.")

Imports Dung reussis.
Utilitaires prets.

Contexte theorique : Knaster-Tarski et grounded extension

La fonction caracteristique de Dung

Pour un cadre d’argumentation AF, on definit l’operateur

F(S) = { a dans AF | S defend a }

ou ” a est defendu par S ” signifie : tout attaquant de a est attaque par au moins un argument de S.

• Complete(S) := S conflict-free ET S inclus dans F(S) ET F(S) inclus dans S <=> F(S) = S (point fixe de F).
• grounded(AF) = plus petit point fixe de F (Dung 1995, Proposition 11).

Knaster-Tarski sur le treillis (Set alpha, inclus)

F est monotone : S inclus dans T => F(S) inclus dans F(T). Le treillis (Set alpha, inclus) etant complet, le theoreme de Knaster-Tarski garantit l’existence d’un plus petit point fixe :

grounded = F.lfp = intersection { S | F(S) inclus dans S }    (le plus petit pre-point-fixe)

et l’iteration depuis le bas converge :

ensemble vide inclus dans F(ensemble vide) inclus dans F^2(ensemble vide) inclus dans ... inclus dans F^n (ensemble vide) = grounded    pour n >= |alpha|

Ce que le lake Lean 4 argumentation_lean/ formalise

Theoreme Lean	Signification	Fichier:ligne
af.characteristic.map_lfp (via OrderHom.lfp)	grounded = F.lfp (Knaster-Tarski)	Characteristic.lean:31-37
grounded_fixed	F(grounded) = grounded	Grounded.lean:51-53
grounded_defends_iff_mem	a dans grounded <=> grounded defend a	Grounded.lean:57-65
grounded_least_complete	toute extension complete contient grounded	Grounded.lean:71-77
F_preserves_admissible	Admissible S => Admissible (F S) (Prop. 7 Dung)	Grounded.lean:97-103

Zero sorry : les modules (Basic, Characteristic, Extensions, Fundamental, Grounded) sont exempts de sorry au dernier lake build SUCCESS du repo.

---

Exercice 1 : Grounded extension - Python naif vs TweetyProject

Objectif. Implementer grounded_python(af) qui itere F(S) depuis S = ensemble vide jusqu’au point fixe, et comparer avec SimpleGroundedReasoner().getModel(af).

Trois cadres de test : 1. Diamant : a -> b, a -> c, b -> d, c -> d (le classique - a est la source, d la cible, deux chemins). 2. Cycle impair 3 : a -> b, b -> c, c -> a (le cas degenerescent - aucun argument n’est inattaque). 3. Symetrie 2x2 : a <-> b, c <-> d, a <-> c, b <-> d (le debat indecidable).

Indice. Pour la representation Python, utiliser des set Python de noms d’arguments et une fonction d’attaque attacks[(src, tgt)].

# Exercice 1 : Grounded extension Python naif vs TweetyProject

def grounded_python(noms, attaques):
    # TODO etudiant : implementer l iteration de F(S) = {a | S defend a}
    # Etape 1 : construire le dictionnaire d attaques (src -> set(tgts))
    # Etape 2 : pour chaque a, calculer attackers[a] = set(src attaquant a)
    # Etape 3 : iterer S = F(S) jusqu a point fixe, en partant de l ensemble vide
    pass

diamant = (["a","b","c","d"], [("a","b"),("a","c"),("b","d"),("c","d")])
cycle3  = (["a","b","c"], [("a","b"),("b","c"),("c","a")])
sym22   = (["a","b","c","d"], [("a","b"),("b","a"),("c","d"),("d","c"),("a","c"),("c","a"),("b","d"),("d","b")])

for nom_cadre, (noms, atts) in [("Diamant", diamant), ("Cycle3", cycle3), ("Sym22", sym22)]:
    af, _ = construire_af(noms, atts)
    py_result = grounded_python(noms, atts)
    tweety_result = noms_extension(SimpleGroundedReasoner().getModel(af))
    py_sorted = sorted(py_result) if py_result else None
    match = "OK" if py_sorted == tweety_result else "DIFF"
    print(f"  {match:5s} {nom_cadre:10s} Python={py_sorted} Tweety={tweety_result}")

  DIFF  Diamant    Python=None Tweety=['a', 'd']
  DIFF  Cycle3     Python=None Tweety=[]
  DIFF  Sym22      Python=None Tweety=[]

Solution exercice 1

L’implementation iterative directe de F(S) = {a | S defend a} converge vers la grounded extension en au plus |noms| etapes (chaque etape elimine au moins un attaquant, donc la suite F^k(ensemble vide) est strictement croissante jusqu’au point fixe).

# Solution complete : grounded Python naif

def grounded_python(noms, attaques):
    """Grounded extension par iteration F(S) depuis l ensemble vide.

    F(S) = {a | attackers[a] inclus dans atk_in(S)}
       ou attackers[a] = ensemble des attaquants de a,
       et atk_in(S) = cibles d attaques issues de S.

    Monotonie de F garantit la convergence en O(|noms|) etapes
    (Knaster-Tarski sur treillis complet (Set alpha, inclus)).
    """
    attackers = {a: set() for a in noms}
    for src, tgt in attaques:
        attackers[tgt].add(src)

    S = set()
    while True:
        atk_from_S = {tgt for src, tgt in attaques if src in S}
        new_S = {a for a in noms if attackers[a] <= atk_from_S}
        if new_S == S:
            return S
        S = new_S

for nom_cadre, (noms, atts) in [("Diamant", diamant), ("Cycle3", cycle3), ("Sym22", sym22)]:
    af, _ = construire_af(noms, atts)
    py_result = sorted(grounded_python(noms, atts))
    tweety_result = noms_extension(SimpleGroundedReasoner().getModel(af))
    match = "OK" if py_result == tweety_result else "DIFF"
    print(f"  {match:5s} {nom_cadre:10s} Python={py_result}  Tweety={tweety_result}")

  OK    Diamant    Python=['a', 'd']  Tweety=['a', 'd']
  OK    Cycle3     Python=[]  Tweety=[]
  OK    Sym22      Python=[]  Tweety=[]

---

Exercice 2 : Convergence numerique vers le point fixe (Knaster-Tarski)

Objectif. Afficher la suite F^0(ensemble vide), F^1(ensemble vide), ..., F^k(ensemble vide) pour un cadre, et montrer qu’elle est monotone croissante et se stabilise au grounded.

Lien avec le lake Lean. - af.characteristic.map_lfp (Characteristic.lean:31-37) prouve que F.lfp = grounded est un point fixe. - OrderHom.lfp_le (Mathlib) prouve que F.lfp est le plus petit pre-point-fixe, donc pour tout S tel que F(S) inclus dans S, on a F.lfp inclus dans S. - L’iteration depuis l’ensemble vide converge en au plus |alpha| etapes (cas fini) car chaque itere est admissible (via F_preserves_admissible, Grounded.lean:97-103) et la chaine ensemble vide dans F(ensemble vide) dans F^2(ensemble vide) dans ... ne peut pas exceder |alpha|+1 termes.

Indice. Modifier grounded_python pour qu’elle retourne la liste des iteres au lieu du seul point fixe. Tester d’abord sur la chaine transitive a -> b, b -> c, a -> c (le cas ou chaque etape ajoute UN argument, illustrant clairement la convergence monotone).

# Exercice 2 : Knaster-Tarski numerique

chaine = (["a","b","c"], [("a","b"),("b","c"),("a","c")])

def iteres_F(noms, attaques):
    # TODO etudiant : retourner la liste des iteres (incluant le point fixe)
    # Indice : demarrer avec [set()] puis appliquer F tant que F(S) != S
    pass

print("Suite F^k(ensemble vide) pour la chaine transitive :")
iteres = iteres_F(*chaine)
if iteres:
    for k, S in enumerate(iteres):
        print(f"  F^{k}(ensemble vide) = {sorted(S)}")
else:
    print("  Exercice a completer")

Suite F^k(ensemble vide) pour la chaine transitive :
  Exercice a completer

Solution exercice 2

La suite F^k(ensemble vide) est monotone croissante : F^k(ensemble vide) inclus dans F^(k+1)(ensemble vide) pour tout k. Knaster-Tarski garantit la stabilisation en au plus |alpha| etapes (la chaine ne peut pas contenir deux memes termes, sinon elle bouclerait et F ne serait pas monotone).

# Solution complete : iteres F

def iteres_F(noms, attaques):
    """Liste des iteres F^k(ensemble vide) jusqu au point fixe.

    Proprietes observables :
      - len(liste) <= |noms| + 1 (Knaster-Tarski, cas fini).
      - S_k inclus dans S_{k+1} (monotonie de F).
      - S_dernier = grounded (point fixe, lake Lean Grounded.lean:51-53).
    """
    attackers = {a: set() for a in noms}
    for src, tgt in attaques:
        attackers[tgt].add(src)

    suites = [set()]
    S = set()
    while True:
        atk_from_S = {tgt for src, tgt in attaques if src in S}
        new_S = {a for a in noms if attackers[a] <= atk_from_S}
        if new_S == S:
            return suites
        S = new_S
        suites.append(S)

for nom_cadre, (noms, atts) in [("Chaine", chaine), ("Diamant", diamant), ("Cycle3", cycle3), ("Sym22", sym22)]:
    iteres = iteres_F(noms, atts)
    af, _ = construire_af(noms, atts)
    tweety_grounded = noms_extension(SimpleGroundedReasoner().getModel(af))
    print(f"--- {nom_cadre} ---")
    for k, S in enumerate(iteres):
        print(f"  F^{k}(ensemble vide) = {sorted(S)}")
    print(f"  Converge en {len(iteres)-1} etapes vers {sorted(iteres[-1])}")
    print(f"  Tweety confirme : grounded = {tweety_grounded}")
    assert sorted(iteres[-1]) == tweety_grounded, "Mismatch Python/Tweety !"
print("OK : les quatre cadres convergent, et l iteration rejoint la grounded Tweety.")

--- Chaine ---
  F^0(ensemble vide) = []
  F^1(ensemble vide) = ['a']
  Converge en 1 etapes vers ['a']
  Tweety confirme : grounded = ['a']
--- Diamant ---
  F^0(ensemble vide) = []
  F^1(ensemble vide) = ['a']
  F^2(ensemble vide) = ['a', 'd']
  Converge en 2 etapes vers ['a', 'd']
  Tweety confirme : grounded = ['a', 'd']
--- Cycle3 ---
  F^0(ensemble vide) = []
  Converge en 0 etapes vers []
  Tweety confirme : grounded = []
--- Sym22 ---
  F^0(ensemble vide) = []
  Converge en 0 etapes vers []
  Tweety confirme : grounded = []
OK : les quatre cadres convergent, et l iteration rejoint la grounded Tweety.

---

Exercice 3 : Le piege - implementation naive non monotone

Objectif. Construire un cadre et une variante naive de F qui diverge de la grounded extension certifiee par Tweety/Lean.

Le piege classique. La definition correcte est

F(S) = { a | TOUS les attaquants de a sont attaques par S }

qu’on peut reecrire attackers[a] inclus dans atk_from(S). Une variante naive consiste a ecrire

F_naive(S) = { a | AU MOINS UN attaquant de a est dans S }

i.e. attackers[a] inter S non vide. Cette variante n’est PAS monotone : sur le cadre a <-> b, on a F_naive({a}) = {b} puis F_naive({b}) = {a} puis F_naive({a}) = {b} - oscillation. La grounded extension est pourtant {} (les deux s’attaquent, aucun n’est defendu), et c’est ce que renvoie SimpleGroundedReasoner.

Pourquoi la garantie du lake Lean l’exclut. Le lake formalise F : Set alpha ->o Set alpha comme morphisme d’ordre (Characteristic.lean:31 dont le champ monotone' prouve S inclus dans T => F(S) inclus dans F(T)). Knaster-Tarski (OrderHom.lfp) n’est invocable QUE parce que F est monotone. La variante naive ci-dessus n’est PAS un morphisme d’ordre - donc Knaster-Tarski ne s’applique pas, et il n’y a aucune raison que l’iteration depuis l’ensemble vide converge vers quoi que ce soit de canonique.

Indice. Implementer grounded_naive_buggy(noms, attaques) avec la mauvaise definition, iterer depuis l’ensemble vide, montrer qu’on oscille ou qu’on atterrit ailleurs que sur la grounded reelle, puis comparer avec SimpleGroundedReasoner.

# Exercice 3 : Le piege - variante naive non monotone

# Cadre de demonstration : chaine transitive a -> b, b -> c, a -> c
# La grounded correcte est {a} (c est attaque par a ET b, donc pas defendu).
# La variante naive inclut {a, b, c} car attackers[b] inter {a} != vide,
# attackers[c] inter {a} != vide, etc. -- sur-acceptation sans base theorique.
chaine = (["a","b","c"], [("a","b"),("b","c"),("a","c")])

def grounded_naive_buggy(noms, attaques, max_iter=20):
    # TODO etudiant : iterer avec la MAUVAISE definition
    # Indice : F_piege(S) = {a | attackers[a] inter S non vide}
    # Tester sur le cadre chaine (a -> b -> c, a -> c)
    # Observer l ecart avec la grounded correcte
    pass

print("Variant naive sur le cadre chaine (a -> b -> c, a -> c) :")
resultat = grounded_naive_buggy(*chaine)
if resultat is not None:
    print(f"  Atterrit sur : {sorted(resultat)}")
    af, _ = construire_af(*chaine)
    tweety_grounded = noms_extension(SimpleGroundedReasoner().getModel(af))
    print(f"  Tweety grounded = {tweety_grounded}")
    print(f"  Match : {sorted(resultat) == tweety_grounded}")
else:
    print("  Exercice a completer")

Variant naive sur le cadre chaine (a -> b -> c, a -> c) :
  Exercice a completer

Solution exercice 3

La variante F_piege(S) = {a | attackers[a] inter S non vide} n’est PAS monotone : sur un conflit symetrique a <-> b, F_piege({a}) = {b} puis F_piege({b}) = {a}, et l’iteration oscille indefiniment. Knaster-Tarski ne s’applique pas (pas de monotonie), donc rien ne garantit la convergence.

La definition mathematique du grounded reste immuable : c’est le plus petit point fixe de F au sens de Knaster-Tarski. Le lake Lean formalise cette definition (Grounded.lean:51-53 grounded_fixed), et TweetyProject l’implemente. Une implementation qui s’en ecarte donne un resultat qui n’est plus la grounded extension, par definition.

Note pedagogique. Le contraste se voit en testant la variante naive sur diverses valeurs initiales S, pas seulement S = ensemble vide : F_piege({a}) peut inclure des arguments non-defendables que la grounded correcte rejette. C’est ce que montre la cellule suivante sur la chaine transitive.

# Solution complete : variante naive - sur-acceptation sans base theorique

def grounded_naive_buggy(noms, attaques, max_iter=10):
    """F_piege(S) = {a | attackers[a] inter S non vide} - non monotone.

    Renvoie (suite_des_iteres, dernier_terme, oscille_ou_non).
    """
    attackers = {a: set() for a in noms}
    for src, tgt in attaques:
        attackers[tgt].add(src)

    S = set()
    suites = [set()]
    for _ in range(max_iter):
        new_S = {a for a in noms if attackers[a] & S}  # Mauvaise definition
        suites.append(new_S)
        if new_S == S:
            return suites, S, False
        S = new_S
    return suites, S, True

# Demonstration : sur la chaine transitive, partant de S = {a}
# (et non de l ensemble vide), la variante naive SUR-ACCEPTE {b, c}.
print("=== Chaine transitive (a -> b -> c, a -> c) ===")
print("Variante naive F_piege(S) = {a | attackers[a] inter S non vide} :")
print()
print("Depart depuis l ensemble vide :")
suites, last, oscille = grounded_naive_buggy(*chaine, max_iter=8)
for k, S in enumerate(suites):
    print(f"  F_piege^{k}(ensemble vide) = {sorted(S)}")
print(f"  -> point fixe trivial {sorted(last)} (par accident)")
print()
print("Depart depuis S = {a} :")
noms, atts = chaine
attackers = {a: set() for a in noms}
for src, tgt in atts:
    attackers[tgt].add(src)
S = {"a"}
print(f"  F_piege({{a}}) = {sorted(a for a in noms if attackers[a] & S)}")
S = {"a", "b", "c"}
print(f"  F_piege({{a,b,c}}) = {sorted(a for a in noms if attackers[a] & S)}")
print()

af, _ = construire_af(*chaine)
tweety_grounded = noms_extension(SimpleGroundedReasoner().getModel(af))
print(f"Tweety grounded (correct, F monotone) = {tweety_grounded}")
print(f"F (correcte) depuis {{a}}            = {sorted(a for a in noms if attackers[a] <= {tgt for src, tgt in atts if src == 'a'})}")
print()
print("Conclusion : la variante naive n'est PAS monotone.")
print("  - F_piege({{a}}) inclut {{b, c}} (a attaque b, a attaque c).")
print("  - Mais b n'est pas defendu (a attaque b sans defense) ;")
print("    c est attaque par a ET b -- il faudrait que S defende c.")
print("  - La grounded correcte grounded = {{a}}.")
print()
print("Knaster-Tarski n'est invocable QUE pour F monotone (OrderHom).")
print("Le lake Lean le formalise (Characteristic.lean:31-37 champ monotone prime).")
print("TweetyProject implemente F monotone, donc livre la grounded correcte.")

=== Chaine transitive (a -> b -> c, a -> c) ===
Variante naive F_piege(S) = {a | attackers[a] inter S non vide} :

Depart depuis l ensemble vide :
  F_piege^0(ensemble vide) = []
  F_piege^1(ensemble vide) = []
  -> point fixe trivial [] (par accident)

Depart depuis S = {a} :
  F_piege({a}) = ['b', 'c']
  F_piege({a,b,c}) = ['b', 'c']

Tweety grounded (correct, F monotone) = ['a']
F (correcte) depuis {a}            = ['a']

Conclusion : la variante naive n'est PAS monotone.
  - F_piege({{a}}) inclut {{b, c}} (a attaque b, a attaque c).
  - Mais b n'est pas defendu (a attaque b sans defense) ;
    c est attaque par a ET b -- il faudrait que S defende c.
  - La grounded correcte grounded = {{a}}.

Knaster-Tarski n'est invocable QUE pour F monotone (OrderHom).
Le lake Lean le formalise (Characteristic.lean:31-37 champ monotone prime).
TweetyProject implemente F monotone, donc livre la grounded correcte.

---

Conclusion

Resultats cles

Verdict	Constat
Equivalence Python/Tweety	L’implementation iterative directe de F depuis l’ensemble vide rejoint SimpleGroundedReasoner sur les 3 cadres de test (diamant, cycle3, sym22).
Knaster-Tarski numerique	La suite F^k(ensemble vide) est strictement croissante, se stabilise en au plus \|alpha\| etapes, et le point fixe coincide avec la grounded certifiee.
Piege identifie	La variante F_piege(S) = {a \| attackers[a] inter S non vide} n’est PAS monotone, donc Knaster-Tarski ne s’applique pas - elle peut osciller et ne livre plus la grounded.

Ce que le lake Lean 4 argumentation_lean/ certifie

• F est monotone en tant que OrderHom (Characteristic.lean:31-37).
• grounded = F.lfp est le plus petit point fixe (Knaster-Tarski via OrderHom.lfp).
• Toute extension complete contient le grounded (grounded_least_complete, Grounded.lean:71-77).
• F preserve l’admissibilite (F_preserves_admissible, Grounded.lean:97-103, cle de la construction iterative).
• Modules, zero sorry au dernier lake build SUCCESS.
• Le lake definit Preferred/Stable (Extensions.lean:50,55) et prouve leurs inclusions vers Complete, mais ne certifie ni l’existence d’extensions preferred/stable ni leur calcul – ces semantiques restent calculees par Tweety (oracle Java non certifie).

Pont avec les notebooks voisins

• Tweety-5-Abstract-Argumentation.ipynb : introduction aux semantiques Dung (grounded, preferred, stable, complete) en Python/Tweety.
• Tweety-5b-Lean-Argumentation.ipynb : kernel lean4-wsl natif, execute les theoremes du lake directement.
• Tweety-12-Grounded-Via-TweetyProject.ipynb (ce notebook) : pont pedagogique qui montre le lien entre l’implementation Java certifiee (TweetyProject) et la formalisation Lean 4 (lake argumentation_lean/), avec exercice explicite sur la monotonie (cle de Knaster-Tarski).

Prochaines etapes

• Notebook Tweety-13 (a venir) : extensions certifiees pour ASPIC+ / DeLP / ABA - branches de l’argumentation structuree.
• Explorer OrderHom.lfp_le directement dans un kernel lean4-wsl pour voir la preuve formelle que l’iteration F^k(ensemble vide) converge.

---

Navigation : <- Tweety-11-Causal | Index