Truth Maintenance System (JTMS) déterministe

Navigation : << 4-capstone | README | Tweety ->

Le rung 2-formal delegue la preuve logique a un solveur externe (Tweety, JVM/JPype) : une fois une formule etablie, elle le reste. C’est le regime monotone – la verite ne se retracte pas.

Mais l’analyse argumentative reelle est non-monotone : un nouvel élément (un sophisme detecte sur une premisse, un temoin discredite) peut invalider une conclusion auparavant tenue pour vraie. Maintenir un etat de croyance coherent sous de telles revisions est précisément le problème qu’un Truth Maintenance System (Doyle, 1979 ; McAllester, de Kleer) resout. Ce rung implemente un JTMS from scratch en pur stdlib Python : croyances, justifications IN/OUT, propagation par point fixe, detection de circularite (odd loops) et cascade de retractation.

Aucun LLM, aucune JVM, aucun solveur externe : l’objet pedagogique est la mecanique du raisonnement non-monotone – la brique algorithmique sur laquelle s’appuient la revision de croyances AGM et les sémantiques d’argumentation.

1. Introduction : raisonnement non-monotone et maintien de croyances

En logique monotone (modus ponens, SAT), ajouter un fait ne retire jamais une conclusion : si p, p => q |- q, alors q reste etabli quoi qu’on ajoute ensuite. C’est le regime du rung 2-formal.

Le raisonnement non-monotone casse cette garantie. Un exemple concret :

  1. « Un expert affirme que X est vrai. » (premisse P)
  2. « Si un expert affirme X, alors X est vrai. » (règle)
  3. Donc X est vrai (conclusion C, derivee de P).

Puis un detecteur de sophismes signale que la premisse P est un appel a l’autorite : P est discreditee. La conclusion C doit alors etre retractee – alors même qu’elle avait ete correctement derivee. C’est une revision, pas une erreur de logique.

Un JTMS (Justification-based Truth Maintenance System) maintient un tel etat de croyance revisable. Chaque croyance est etiquetee IN (activement soutenue) ou OUT (non soutenue). Les etiquettes se recalculent par propagation dans un graphe de justifications. Retracter une croyance fondatrice declenche une cascade : toutes les croyances qui en dependaient basculent OUT a leur tour.

Concept Definition Rôle dans ce rung
Croyance (belief) Un noeud du graphe, etiquete IN ou OUT Unite de raisonnement
Justification Règle : conclusion est IN ssi tout in_list est IN et tout out_list est OUT Lien de support
Premisse Croyance IN inconditionnellement (justification vide) Fondation
Etiquetage Calcul du statut IN/OUT de chaque croyance Point fixe monotone
Cascade Retracter une croyance -> bascule de ses dependants Propagation non-monotone
Odd loop Cycle de support positif (A soutient B soutient A) Anomalie a detecter

Provenance : ce moteur a un original au tronc

Le moteur de ce carnet est une reecriture pedagogique du module argumentation_analysis/services/jtms/jtms_core.py du tronc EPITA, integre du projet etudiant 1.4.1-JTMS (auteur original @ThomasLeguere). Le tronc en porte une version enrichie : croyance tri-etat (True / False / None), detection de circularite par composantes fortement connexes (networkx, degradation gracieuse si absent), trace de retractation, explication d’une croyance, et visualisation HTML (pyvis).

Ce carnet garde volontairement un moteur inline et stdlib — aucune dependance externe, une detection de circularite ecrite a la main, executable partout — et en distille deux instruments : la chaine de retractation (retraction_chain, section 4) et l’explication d’une croyance (explain_belief, section 6). Ils rendent la cascade tracable comme donnee, au lieu de se lire a l’oeil sur deux etiquetages.

Source : tronc EPITA jsboigeEpita/2025-Epita-Intelligence-Symbolique, argumentation_analysis/services/jtms/jtms_core.py, commit ecfd9b9c31 (instruments d’origine : get_retraction_chain, explain_belief, visualize).

2. Le modèle de données : croyances et justifications IN/OUT

Une justification est un triplet :

  • in_list : liste de croyances qui doivent toutes etre IN ;
  • out_list : liste de croyances qui doivent toutes etre OUT ;
  • conclusion : la croyance soutenue.

La justification est valide ssi ses deux conditions tiennent simultanement. Une croyance est IN des qu’au moins une de ses justifications est valide. Une premisse est une justification aux listes vides : sa conclusion est IN sans condition (le point d’ancrage du raisonnement).

La cellule ci-dessous définit le moteur JTMS complet (modèle de données + etiquetage + retractation + detection de circularite). Les sections suivantes demontrent chaque mécanisme.

# Cellule [2] - Le moteur JTMS complet (pur stdlib, 0 dependance externe)
from dataclasses import dataclass, field
from typing import List, Dict, Set


@dataclass
class Justification:
    """Une regle de support : `conclusion` est IN ssi
    tout in_list est IN et tout out_list est OUT."""
    conclusion: str
    in_list: List[str] = field(default_factory=list)
    out_list: List[str] = field(default_factory=list)


class JTMS:
    """Justification-based Truth Maintenance System (Doyle 1979, well-founded).

    Les croyances vivent dans un ensemble de noms (str). Les justifications
    forment un graphe oriente. L'etiquetage est un point fixe monotone :
    toutes les croyances partent OUT, puis sont promues IN quand une
    justification valide est trouvee, jusqu'a stabilite.
    """

    def __init__(self):
        self.beliefs: Set[str] = set()
        self.justifications: List[Justification] = []

    def add_belief(self, name: str) -> None:
        self.beliefs.add(name)

    def add_premise(self, name: str) -> None:
        """Une premisse = croyance IN inconditionnellement (listes vides)."""
        self.add_belief(name)
        self.justifications.append(Justification(name, [], []))

    def add_justification(self, conclusion: str,
                          in_list: List[str] = None,
                          out_list: List[str] = None) -> None:
        in_list = in_list or []
        out_list = out_list or []
        self.add_belief(conclusion)
        for b in in_list + out_list:
            self.add_belief(b)
        self.justifications.append(Justification(conclusion, in_list, out_list))

    # --- Etiquetage (well-founded, point fixe monotone) ---
    def label(self) -> Dict[str, str]:
        """Calcule le statut IN/OUT de chaque croyance.

        Monotone : on ne fait que des transitions OUT -> IN, le nombre de
        croyances borne les iterations -> convergence garantie. Les odd loops
        (cycles de support positif) ne sont jamais promus -> restent OUT.
        """
        status = {b: "OUT" for b in self.beliefs}
        changed = True
        while changed:
            changed = False
            for b in self.beliefs:
                if status[b] != "IN":
                    for j in self.justifications:
                        if j.conclusion == b and \
                           all(status[x] == "IN" for x in j.in_list) and \
                           all(status[x] == "OUT" for x in j.out_list):
                            status[b] = "IN"
                            changed = True
                            break
        return status

    # --- Retractation (declenche la cascade au prochain label) ---
    def retract(self, name: str) -> None:
        """Retire toutes les justifications dont la conclusion est `name`.
        Les croyances qui en dependaient perdront leur support -> basculent OUT
        au prochain etiquetage (cascade non-monotone)."""
        self.justifications = [j for j in self.justifications if j.conclusion != name]

    # --- Chaine de retractation (instrument distille du tronc) ---
    def _positive_deps(self) -> Dict[str, Set[str]]:
        """Aretes de dependance POSITIVE : premisse -> conclusion.

        Le `out_list` n'y figure pas : il exprime une defense, pas un soutien.
        """
        deps: Dict[str, Set[str]] = {b: set() for b in self.beliefs}
        for j in self.justifications:
            for x in j.in_list:
                deps.setdefault(x, set()).add(j.conclusion)
        return deps

    def retraction_chain(self, name: str) -> List[Dict[str, object]]:
        """Retracte `name` et rend la cascade **ordonnee**, comme donnee.

        Adapte de `get_retraction_chain` du tronc (services/jtms) : la-bas la
        trace s'accumule au fil de la propagation ; ici l'etiquetage est
        recalcule globalement, donc la chaine est le diff des etiquettes
        (`label()` avant / apres) parcouru en largeur depuis le declencheur.

        Rend une liste de `{'belief', 'cause', 'profondeur'}` : la profondeur
        vaut 0 pour la croyance retractee elle-meme, puis 1 pour ses dependants
        directs, etc. `cause` est la croyance dont la chute a emporte celle-ci
        (`None` pour le declencheur).
        """
        before = self.label()
        self.retract(name)
        after = self.label()
        deps = self._positive_deps()

        chain: List[Dict[str, object]] = [
            {"belief": name, "cause": None, "profondeur": 0}
        ]
        vus = {name}
        frontiere = [name]
        profondeur = 0
        while frontiere:
            profondeur += 1
            suivante = []
            for cause in frontiere:
                for concl in sorted(deps.get(cause, ())):
                    if concl in vus or concl == name:
                        continue
                    if before.get(concl) == "IN" and after.get(concl) == "OUT":
                        chain.append({
                            "belief": concl,
                            "cause": cause,
                            "profondeur": profondeur,
                        })
                        vus.add(concl)
                        suivante.append(concl)
            frontiere = suivante
        return chain

    # --- Detection de circularite (odd loops) ---
    def find_circular(self) -> Set[str]:
        """Croyances OUT dont le seul support est un cycle positif (odd loop).

        On construit le graphe de dependance POSITIVE (on ignore le out_list,
        car un odd loop est un cycle de soutiens mutuels), on en calcule les
        composantes fortement connexes (Tarjan), et on signale les croyances
        OUT appartenant a un cycle non trivial (ou une auto-boucle).
        """
        st = self.label()
        deps = {b: set() for b in self.beliefs}
        for j in self.justifications:
            for x in j.in_list:
                deps[j.conclusion].add(x)

        index_counter = [0]
        stack = []
        on_stack = set()
        index = {}
        lowlink = {}
        sccs = []

        def strongconnect(v):
            index[v] = lowlink[v] = index_counter[0]
            index_counter[0] += 1
            stack.append(v)
            on_stack.add(v)
            for w in deps[v]:
                if w not in index:
                    strongconnect(w)
                    lowlink[v] = min(lowlink[v], lowlink[w])
                elif w in on_stack:
                    lowlink[v] = min(lowlink[v], index[w])
            if lowlink[v] == index[v]:
                comp = []
                while True:
                    w = stack.pop()
                    on_stack.discard(w)
                    comp.append(w)
                    if w == v:
                        break
                sccs.append(comp)

        for v in self.beliefs:
            if v not in index:
                strongconnect(v)

        circular = set()
        for comp in sccs:
            is_cycle = len(comp) > 1 or (len(comp) == 1 and comp[0] in deps[comp[0]])
            if is_cycle and all(st[b] == "OUT" for b in comp):
                circular.update(comp)
        return circular

    # --- Explication d'une croyance (instrument distille du tronc) ---
    def _fondations_perdues(self, name: str, vus=None) -> List[str]:
        """Remonte les fondations OUT sous `name` : la cause racine de la chute.

        Une fondation est une croyance sans justification propre — une regle
        retiree, ou une premisse jamais posee. On descend par les aretes
        positives et on s'arrete sur les cycles.
        """
        vus = vus if vus is not None else set()
        if name in vus:
            return []
        vus.add(name)
        st = self.label()
        regles = [j for j in self.justifications if j.conclusion == name]
        if not regles and st.get(name) == "OUT":
            return [name]
        racines: List[str] = []
        for j in regles:
            for premisse in j.in_list:
                if st.get(premisse) == "OUT":
                    racines.extend(self._fondations_perdues(premisse, vus))
        return sorted(set(racines))

    def explain_belief(self, name: str) -> str:
        """Explique l'etiquetage d'une croyance, regle par regle.

        Adapte de `explain_belief` du tronc : chaque regle concluant vers
        `name` liste ses premices IN/OUT et son verdict. Le verdict distingue
        trois cas, comme le tri-etat du tronc — `valide`, `non concluante
        (circularite)` pour une croyance prise dans un odd loop, `invalide`
        pour un support simplement defait. Une croyance OUT nomme enfin la
        fondation perdue qui a emporte la cascade.
        """
        st = self.label()
        circ = self.find_circular()
        regles = [j for j in self.justifications if j.conclusion == name]
        etat = st.get(name, "?")
        lignes = [f"{name} = {etat}"]
        for j in regles:
            in_status = ", ".join(f"{b} ({st.get(b, '?')})" for b in j.in_list) or "-"
            out_status = ", ".join(f"{b} ({st.get(b, '?')})" for b in j.out_list) or "-"
            soutenue = (all(st.get(b) == "IN" for b in j.in_list)
                        and all(st.get(b) == "OUT" for b in j.out_list))
            if soutenue and not j.in_list and not j.out_list:
                verdict = "valide (premisse : soutien inconditionnel)"
            elif soutenue:
                verdict = "valide"
            elif name in circ:
                verdict = "non concluante (circularite)"
            else:
                verdict = "invalide"
            lignes.append(
                f"  regle : IN=[{in_status}] OUT=[{out_status}] -> {verdict}"
            )
        if not regles:
            lignes.append("  aucune regle : croyance sans soutien")
        if etat == "OUT":
            racines = self._fondations_perdues(name)
            if racines:
                lignes.append(f"  fondation perdue : {', '.join(racines)}")
        return "\n".join(lignes)

    def summary(self) -> str:
        st = self.label()
        lines = [f"  {b:20s} = {st[b]}" for b in sorted(self.beliefs)]
        circ = self.find_circular()
        if circ:
            lines.append(f"  --- circularite detectee : {sorted(circ)}")
        return "\n".join(lines)


print("Moteur JTMS charge (Justification, JTMS) + 2 instruments distilles du tronc (retraction_chain, explain_belief).")
Moteur JTMS charge (Justification, JTMS) + 2 instruments distilles du tronc (retraction_chain, explain_belief).

3. L’algorithme d’etiquetage : un point fixe monotone

L’etiquetage label() suit un schema classique de sémantique bien-fondee (well-founded) :

  1. Initialisation : toutes les croyances sont OUT.
  2. Promotion : une croyance devient IN si l’une de ses justifications est valide (tout son in_list est IN, tout son out_list est OUT).
  3. Itération : on repete jusqu’a ce qu’aucune promotion n’ait lieu (point fixe).

L’étape 2 ne fait que des transitions OUT -> IN. Comme le nombre de croyances est fini, le processus converge necessairement. C’est cette monotonicite qui garantit la terminaison et qui laisse les odd loops a OUT (un cycle de soutiens mutuels ne possede pas de fondation independante, donc aucune croyance du cycle n’est jamais promue).

Construisons une chaîne lineaire : la premisse A soutient B, qui soutient C.

# Cellule [4] - Etiquetage sur une chaine lineaire acyclique
t = JTMS()
t.add_premise("A")                          # A = premisse (IN inconditionnel)
t.add_justification("B", in_list=["A"])     # B IN ssi A IN
t.add_justification("C", in_list=["B"])     # C IN ssi B IN

print("Chaine A -> B -> C :")
print(t.summary())
Chaine A -> B -> C :
  A                    = IN
  B                    = IN
  C                    = IN

Interpretation : etiquetage acyclique

Sortie attendue : A = IN, B = IN, C = IN. La propagation est partie de la premisse A (IN inconditionnel), a promu B (sa justification A est IN), puis C (sa justification B est devenu IN), et s’est stabilisee au point fixe.

C’est exactement un modus ponens en chaîne, mais execute par un moteur de maintien de croyances plutot que par un solveur SAT. La différence essentielle apparaitra en section 4 : ici, retirer A n’est pas une opération interdite – elle declenche une cascade.

Exercice 1 : branchez une alternative (disjonction de soutiens)

Contexte : une croyance peut avoir plusieurs justifications. Elle devient IN des que l’une d’elles est valide. C’est le support disjonctif (OR).

Objectif : ajoutez une deuxieme justification a C : C est IN ssi D est IN, ou D est une nouvelle premisse. Verifiez que si vous retractez B (section 4), C reste IN grace a D.

# Exercice 1 (JTMS) : support disjonctif
# TODO etudiant : ajoutez une premisse 'D' et une justification 'C <- D',
# puis affichez le summary. Etape 1 : declarez D. Etape 2 : reliez C a D.
# Indice : t.add_premise("D") puis t.add_justification("C", in_list=["D"])
resultat = None  # TODO etudiant : t.summary()
print(resultat)
None

4. Retractation et cascade : le coeur non-monotone

La mecanique non-monotone se revele quand on retracte une croyance. retract(name) retire toutes les justifications dont la conclusion est name – la croyance perd alors tout support direct. Au prochain label(), les croyances qui dependaient (transitivement) de name perdent a leur tour leur support et basculent OUT : c’est la cascade.

C’est l’ecart fondamental avec la logique monotone du rung 2-formal : la, une formule etablie l’etait pour toujours ; ici, retracter une fondation defait les conclusions qui en descendaient.

# Cellule [6] - Cascade de retractation, tracee comme donnee
t = JTMS()
t.add_premise("A")
t.add_justification("B", in_list=["A"])
t.add_justification("C", in_list=["B"])

print("AVANT retractation :")
print(t.summary())

print("\nChaine de retractation de A (retraction_chain, distille du tronc) :")
for entree in t.retraction_chain("A"):
    cause = "declencheur" if entree["cause"] is None else f"cause : {entree['cause']}"
    print(f"  profondeur {entree['profondeur']}  {entree['belief']:16s} {cause}")

print("\nAPRES retractation de A :")
print(t.summary())
AVANT retractation :
  A                    = IN
  B                    = IN
  C                    = IN

Chaine de retractation de A (retraction_chain, distille du tronc) :
  profondeur 0  A                declencheur
  profondeur 1  B                cause : A
  profondeur 2  C                cause : B

APRES retractation de A :
  A                    = OUT
  B                    = OUT
  C                    = OUT

Interpretation : la cascade

Sortie attendue : avant retractation, A=B=C=IN. Après, A=B=C=OUT. Retirer le soutien de A a fait chuter B (qui ne tenait qu’a A), puis C (qui ne tenait qu’a B). Le graphe s’est re-etiquete de fondation en sommet.

retraction_chain rend cet ordre comme donnee : A en profondeur 0 (le declencheur), B en profondeur 1 (cause : A), C en profondeur 2 (cause : B). L’ordre de propagation se lit directement, au lieu de se deduire en comparant deux etiquetages — c’est la trace que le tronc porte sous get_retraction_chain, ramenee ici a l’echelle du carnet.

C’est précisément la mecanique qu’il faut pour l’analyse argumentative : quand une premisse est discreditee (par exemple un appel a l’autorite detecte), les conclusions qui s’appuyaient dessus doivent tomber automatiquement, sans qu’on ait a re-deriver la chaîne a la main.

Exercice 2 : predisez la cascade avant de l’executer

Contexte : un graphe en diamant – D soutient B et C, qui soutiennent tous deux E.

Objectif : avant de lancer le code, notez sur papier le statut de B, C, E après retractation de D. Puis codez-le et verifiez.

# Exercice 2 (JTMS) : graphe en diamant, predisez puis verifiez
# TODO etudiant : construisez A(premisse) -> B,C -> E, retractez A, affichez.
# Etape 1 : t.add_premise("A"). Etape 2 : B et C depuis A. Etape 3 : E depuis B et C.
# Etape 4 : t.retract("A"). Etape 5 : print(t.summary()).
# Indice : E a une seule justification in_list=[B, C] (conjonction) ->
#           des que B ou C tombe, E tombe aussi.
resultat = None  # TODO etudiant
print(resultat)
None

5. Detection de circularite : les odd loops

Un piege subtil du raisonnement non-monotone est la circularite de support : si A n’est soutenu que par B, et B que par A, aucune des deux croyances n’a de fondation independante. C’est un odd loop (boucle etrangere).

L’algorithme monotone de la section 3 le gere silencieusement : ni A ni B n’est jamais promu, donc les deux restent OUT. Mais il est crucial de le detecter et de le signaler : une croyance OUT « par manque de fondation » (un fait absent) et une croyance OUT « par circularite » (un defaut de structure) ne signifient pas la même chose. La seconde revele une anomalie de modelisation qu’il faut corriger.

find_circular() construit le graphe des soutiens positifs, en extrait les composantes fortement connexes (algorithme de Tarjan) et signale les croyances OUT appartenant a un cycle.

# Cellule [8] - Odd loop et sa detection
o = JTMS()
o.add_justification("A", in_list=["B"])    # A IN ssi B IN
o.add_justification("B", in_list=["A"])    # B IN ssi A IN  -> cycle A<->B

print("Odd loop A <-> B :")
print(o.summary())
Odd loop A <-> B :
  A                    = OUT
  B                    = OUT
  --- circularite detectee : ['A', 'B']

Interpretation : pourquoi la circularite casse le raisonnement

Sortie attendue : A = OUT, B = OUT, suivis de --- circularite detectee : ['A', 'B']. L’etiquetage a laisse les deux croyances OUT (aucune fondation), et la detection a marque la paire comme circulaire.

Comparez avec une croyance simplement « non soutenue » (une premisse absente) : elle est OUT elle aussi, mais non marquee circulaire. Distinguer ces deux causes d’OUT est la valeur ajoutee de find_circular : la circularite est un defaut de modelisation (le graphe est mal construit), pas un defaut de fait (une information manque). Un moteur TMS industriel rejette un jeu de justifications contenant un odd loop plutot que de l’accepter silencieusement.

Le tronc pousse plus loin : sa fonction visualize() dessine le graphe en HTML interactif (pyvis) pour rendre l’odd loop visible. Ce carnet s’en tient volontairement a la sortie texte pour rester sans dependance externe — la visualisation y est une extension possible, pas une piece du rung.

Exercice 3 : construisez un odd loop de taille 3

Contexte : un cycle de longueur 3 – A <- B, B <- C, C <- A – est lui aussi un odd loop non trivial.

Objectif : construisez-le, verifiez que les trois croyances sont OUT et que find_circular() les signale toutes.

# Exercice 3 (JTMS) : odd loop de taille 3
# TODO etudiant : A <- B, B <- C, C <- A. Affichez le summary.
# Etape 1-3 : trois add_justification formant le cycle. Etape 4 : print(t.summary()).
# Indice : la detection doit retourner {'A','B','C'}.
resultat = None  # TODO etudiant
print(resultat)
None

6. Application : detecter un sophisme et propager la retractation

C’est la demonstration qui relie ce rung a la vocation de la serie. On modelise un argument simple :

  • Premisse : expert_claims_X – « un expert affirme que X est vrai » (un appel a l’autorite potentiel).
  • Règle : si l’expert affirme X, alors X_is_true.
  • Règle : si X est vrai, alors on decide_X.

L’etiquetage initial place les trois croyances IN. Puis un detecteur de sophismes (le rung 1-informal le fait sur du texte reel) identifie la premisse comme un appel a l’autorite. On retracte expert_claims_X ; la cascade defait X_is_true puis decide_X. La conclusion tombe sans intervention manuelle sur la chaîne.

# Cellule [10] - Detecter un sophisme (appel a l'autorite) -> retracter -> propager
t = JTMS()
t.add_premise("expert_claims_X")                        # « un expert affirme X »
t.add_justification("X_is_true", in_list=["expert_claims_X"])
t.add_justification("decide_X", in_list=["X_is_true"])

print("AVANT detection du sophisme :")
print(t.summary())

# Le detecteur de sophismes (rung 1-informal) signale expert_claims_X
# comme un APPEL A L'AUTORITE -> on retracte la croyance compromise.
t.retract("expert_claims_X")

print("\nPourquoi la decision tombe (explain_belief, distille du tronc) :")
print(t.explain_belief("decide_X"))

print("\nAPRES retractation de l'autorite (cascade) :")
print(t.summary())
AVANT detection du sophisme :
  X_is_true            = IN
  decide_X             = IN
  expert_claims_X      = IN

Pourquoi la decision tombe (explain_belief, distille du tronc) :
decide_X = OUT
  regle : IN=[X_is_true (OUT)] OUT=[-] -> invalide
  fondation perdue : expert_claims_X

APRES retractation de l'autorite (cascade) :
  X_is_true            = OUT
  decide_X             = OUT
  expert_claims_X      = OUT

Interpretation : du sophisme a la retractation

Sortie attendue : avant, expert_claims_X = X_is_true = decide_X = IN. Après, les trois sont OUT. La detection d’un seul sophisme a suffit a invalider la conclusion et la decision, parce que le graphe de justifications encodait explicitement qui depend de qui.

C’est la promesse du raisonnement non-monotone outille : la detection d’un sophisme n’est pas une simple etiquette posée sur un texte, c’est un événement qui se propage dans l’etat de croyance et defait ce qui n’etait soutenu que par le sophisme. La section suivante verse cet etat dans le conteneur partage de la serie.

explain_belief nomme la fondation perdue : decide_X tombe parce que sa regle requiert X_is_true, devenue OUT, elle-meme parce que expert_claims_X a perdu sa regle. La retractation du sophisme cesse d’etre un diff a interpreter : elle s’enonce en clair, regle par regle, jusqu’a la croyance qui a lache la premiere.

7. Pont vers l’etat partage

Les croyances etiquetees par le JTMS alimentent le même conteneur partage que tous les rungs enrichissent : l’etat UnifiedAnalysisState du module argumentation_lib (une sous-classe de RhetoricalAnalysisState qui ajoute, entre autres, un champ jtms_beliefs). Le rung 1 y ecrit ses detections informelles, le rung 2 y attache des verdicts formels, le rung 3 y depose le résultat orchestre, et ce rung (5) y verse les croyances non-monotones du JTMS. Aucun LLM requis : on remplit l’etat a partir de notre moteur déterministe.

# Cellule [12] - Pont : verser les croyances JTMS dans UnifiedAnalysisState
from argumentation_lib import UnifiedAnalysisState

# On reconstruit un JTMS propre (etat IN, avant toute retractation)
t = JTMS()
t.add_premise("expert_claims_X")
t.add_justification("X_is_true", in_list=["expert_claims_X"])
t.add_justification("decide_X", in_list=["X_is_true"])

etat = UnifiedAnalysisState(initial_text="Argument modele pour le pont JTMS")
status = t.label()
for nom, statut in status.items():
    soutiens = [j.in_list for j in t.justifications if j.conclusion == nom]
    etat.add_jtms_belief(name=nom, valid=(statut == "IN"), justifications=soutiens)

print("Croyances JTMS versees dans l'etat partage :")
for bid, bdata in etat.jtms_beliefs.items():
    print(f"  {bid}: {bdata}")
print(f"Total : {len(etat.jtms_beliefs)} croyances non-monotones dans l'etat.")
Croyances JTMS versees dans l'etat partage :
  jtms_1: {'name': 'decide_X', 'valid': True, 'justifications': [['X_is_true']]}
  jtms_2: {'name': 'expert_claims_X', 'valid': True, 'justifications': [[]]}
  jtms_3: {'name': 'X_is_true', 'valid': True, 'justifications': [['expert_claims_X']]}
Total : 3 croyances non-monotones dans l'etat.

8. Conclusion et recapitulatif

Ce rung a ouvert la boite noire du raisonnement non-monotone. La le rung 2-formal deleguait a un solveur externe, ici on a construit le moteur qui maintient un etat de croyance revisable : etiquetage par point fixe monotone, cascade de retractation, detection de circularite.

Tableau recapitulatif

Mécanisme Ce qu’il fait Pourquoi ca compte
Etiquetage IN/OUT Point fixe monotone sur le graphe de justifications Distingue le soutenu du non-soutenu, converge toujours
Cascade de retractation Retirer une fondation defait ses dependants C’est l’essence du non-monotone : retracter != erreur de logique
Detection d’odd loop Signale les cycles de support positif Distingue « manque de fait » et « defaut de modelisation »

Ce que vous avez appris

  • Un JTMS modelise des croyances reliees par des justifications IN/OUT, etiquetees par un calcul de point fixe.
  • Retracter une croyance declenche une cascade qui defait les conclusions non-monotones – exactement ce qu’il faut quand un sophisme discredite une premisse.
  • Les odd loops (cycles de soutiens mutuels) sont des anomalies structurelles qu’un bon moteur detecte plutot que d’accepter silencieusement.

Prochaines étapes

  • Revision de croyances AGM : le JTMS est la brique algorithmique sur laquelle s’appuient les opérations de revision (Alchourron, Gardenfors & Makinson, 1985). La serie Tweety implemente ces opérations dans le solveur (notebook 4).
  • Sémantiques d’argumentation : l’etiquetage IN/OUT est l’ancetre des etiquetages de Dung (IN/OUT/UNDECIDED). Le rung 2-formal section 6 les revisite via le solveur Tweety.
  • Preuve formelle : la correction de l’algorithme de point fixe (terminaison, caracterisation well-founded) se formalise. La serie Lean est le cadre naturel pour cette formalisation.
Retour au sommet