Carnet de distillation : le materiau source est la distillation-outil EPITA 2025 Argumentation, projet 1.4.1-JTMS (issues EPITA #1961 phase 4, pipeline arrete le 15/09). Il complete l’instrument ICT-Argumentation-BeliefTrajectories (Phase B, #7742) : la ou la Phase B suivait la trajectoire de croyances d’un debat sous semantique grounded, ce carnet distille les mecanismes de revision eux-memes — comment un systeme de croyances maintient sa coherence quand une premisse tombe. Trois objets : le JTMS (un seul etat courant, revise par evenement), l’ATMS (tous les environnements d’hypotheses d’un coup), et le pont vers l’AF de Dung deja porte par l’organe ict.argumentation (Phase A, #7336).
Statut epistemique — Sans verdict a ce jour : aucune ligne de la matrice de dissociations ne concerne ce notebook ; son statut epistemique sera porte par la matrice le cas echeant.
Declaration organ-first (regle organ-first-implementation) : ce carnet est une copie pedagogique declaree du projet EPITA 1.4.1-JTMS (fichiers jtms.py, 184 lignes, et atms.py, 83 lignes, mesures firsthand a la tete 487210fb du clone local le 2026-09-22). Le port vit dans l’organe ict/truth_maintenance.py ; sa fidelite est prouvee par execution differentielle contre le code source original : 5 corpus/cas (corpus simple_beliefs avec et sans premisse, cas cycle, ATMS avec purge retroactive, corpus no_justification) produisent des tables byte-identiques — les valeurs affichees dans ce carnet SONT celles de la source. Divergences declarees : pas de networkx (SCC par fermeture d’accessibilite), pas de pyvis (tables au lieu de HTML), pas d’emojis, nom de methode orthographie. Les quirks mesures de la source sont conserves et enseignes, pas corriges (sections 3 et 4).
§1 — Setup
Import des organes de la serie depuis ICT-Series/ (convention de la serie, cf. Phase A/B). Le module ict.truth_maintenance est le port EPITA declare ci-dessus ; ict.argumentation (Phase A, PR #7336 mergeee) fournit l’AF de Dung et la semantique grounded. Aucune dependance hors serie : CPU pur, aucun aleatoire (determinisme complet par construction — il n’y a rien a seeder).
import os, sysICT_ROOT = os.path.abspath('.')if ICT_ROOT notin sys.path: sys.path.insert(0, ICT_ROOT)from ict import argumentation as arg # organe natif Phase A (Dung)from ict import truth_maintenance as tms # port EPITA 1.4.1-JTMS (this grain)# basenames seulement dans les sorties (pas de chemin machine -- regle 6)print('organe argumentation :', os.path.basename(arg.__file__))print('organe truth_maintenance:', os.path.basename(tms.__file__))print('semantiques JTMS/ATMS pretes.')
§2 — Pourquoi reviser : le grounded est statique, la croyance ne l’est pas
La semantique grounded (Phase A) repond a une question instantanee : etant donne un AF complet, quels arguments sont acceptables ? Mais un debat reel est sequentiel et revisable : une premisse tombe (un temoin se reprend), un fait nouveau arrive, et la question devient : que reste-t-il soutenu, et pourquoi ? La Phase B traquait la trajectoire de la collective (l’ordre d’arrivee des arguments change l’extension). Ici on descend d’un cran : la memoire de justification elle-meme.
Un systeme de maintenance de la verite (truth maintenance system, Doyle 1979 ; de Kleer 1986 pour l’ATMS) enregistre pour chaque croyance pourquoi elle tient : une liste de justifications de la forme in:[...] out:[...] -> conclusion. Une croyance est valide s’il existe une justification dont toutes les premisses in sont valides et dont aucune clause out n’est valide. C’est cette seconde clause qui rend le systeme non monotone : retirer une information peut creer une validite (la clause out ne bloque plus). Toute la difference entre JTMS et ATMS tient dans la strategie de calcul : le JTMS maintient un seul etat courant qu’il revise evenement par evenement ; l’ATMS calcule toutes les explications simultanement (sous quels ensembles d’hypotheses chaque noeud tient) et represente l’incoherence comme un nogood. Ce carnet mesure les deux sur les corpus de la source, puis croise avec le grounded de l’organe.
# Rappel statique : l'organe Phase A repond instantanement.af = arg.tweety_bird()print('AF Tweety : arguments', list(af.arguments), '| attaques', list(af.attacks))labeling = arg.grounded_labeling(af)print('grounded :', labeling)# 0='Tweety vole', 1='Tweety ne vole pas', 2='c'est un oiseau'# -> 2 in (rien ne l'attaque), 1 out (attaque par 2), 0 in (son attaquant 1 est out).
Lecture. Le labeling {'0': 'in', '1': 'out', '2': 'in'} (indices selon l’ordre d’affichage) est un fait accompli : l’organe ne dit rien de ce qui se passe si l’argument 2 disparait, ni sous quelles hypotheses 0 serait defendable. C’est precisement l’information que le TMS rajoute : avec des justifications, la chute d’une premisse propage, et l’ATMS sait enumerer les mondes d’hypotheses. La section 5 montrera que les deux lectures se croisent sans se reduire l’une a l’autre.
§3 — JTMS : un etat courant, revisé par evenement
Le corpus simple_beliefs.json de la source EPITA, reproduit en litteraux (il vit aussi dans les tests de l’organe) : A soutient B et C ; B avec C absent soutient D ; C est aussi soutenu par l’absence de B ; B par l’absence de A. On pose A comme premisse et on observe la table des etats — chaque croyance porte un etat tri-state : True (valide), False (invalide), None (inconnu).
table (A pose) : {'A': True, 'B': True, 'C': True, 'D': None}
Justification :
IN : B -> VALID (VALID)
OUT : C -> VALID (VALID)
-> Results: not-VALID
Lecture.{'A': True, 'B': True, 'C': True, 'D': None} — D reste inconnu : sa seule justification exige B valide ET C absent, or C est soutenu par A. La table est celle de la source EPITA, mesuree par execution differentielle (gate 1 des tests) : ce n’est pas une interpretation, c’est le comportement du moteur d’origine. L’explication imprimee au-dessus montre la cause ligne a ligne : la clause OUT : C (VALID) bloque la justification.
Retirons maintenant la premisse : A redevient inconnu. Prediction naive (monotone) : tout s’effondre. Mesure :
t.set_belief_validity('A', None) # la premisse tombetable_sans_A = t.status_table()print('table (A retire):', table_sans_A)print()print(t.explain_belief('B'))# Temoins : la propagation est bien repartie depuis l'evenement, pas recalculee a la volee.assert table_avec_A == {'A': True, 'B': True, 'C': True, 'D': None}assert table_sans_A == {'A': None, 'B': True, 'C': None, 'D': True}
table (A retire): {'A': None, 'B': True, 'C': None, 'D': True}
Justification :
IN : A -> UNKNOWN (not-VALID)
OUT : -
-> Results: not-VALID
Justification :
IN : -
OUT : A -> UNKNOWN (not-VALID)
-> Results: VALID
Lecture — le quirk mesure de la negation-as-failure. Avec A inconnu, Bsurvit via sa seconde justification (out:[A] — l’absence de A suffit), C tombe, et Dremonte (B valide, C absent). C’est le comportement exact de la source (gate 2), et il est pedagogiquement precis : une clause out se lit negation as failure — un etat inconnu satisfait la clause de blocage, exactement comme un etat invalide. Un systeme monotone aurait tout effondre ; le TMS, lui, reorganise la validite. C’est la signature de la revision non monotone, et la raison pour laquelle on ne peut pas se contenter du labeling statique de la section 2.
Et les boucles ? Une croyance qui ne tient que par une boucle de justifications ne doit pas etre mesuree : le moteur marque les composantes fortement connexes non triviales (non_monotonic) et force leur etat a None — un refus de mesurer, pas un zero (meme discipline que la Phase B, #13837).
tc = tms.JTMS(strict=False)tc.add_justification(['B'], [], 'A') # A tient par B...tc.add_justification(['A'], [], 'B') # ...et B par A : boucletc.add_belief('C')tc.set_belief_validity('C', True)print('table :', tc.status_table())print('non_monotonic :', {n: b.non_monotonic for n, b in tc.beliefs.items()})assert tc.status_table() == {'A': None, 'B': None, 'C': True}assert tc.beliefs['A'].non_monotonic and tc.beliefs['B'].non_monotonic
Lecture.A et B restent Noneet portent le marqueur non_monotonic — le moteur sait dire pourquoi il ne mesure pas (gate 3). La detection des cycles utilise une fermeture d’accessibilite (divergence declaree n. 1 : la source appelle networkx, la serie est numpy-only) ; le resultat differentiel est identique.
§4 — ATMS : toutes les hypotheses d’un coup
Le JTMS repond a un scenario. L’ATMS (assumption-based TMS) repond a tous : chaque noeud porte une etiquette — l’ensemble des environnements d’hypotheses sous lesquels il tient. Une hypothese commence avec {elle-meme} ; chaque justification propage le produit cartesien des etiquettes de ses in (en bloquant si une etiquette d’un out est incluse dans l’environnement fusionne) ; la contradiction est un noeud perp dont chaque environnement devient un nogood, purge de toutes les etiquettes. Construisons l’instance de la source : hypotheses p, q ; p -> x ; q et x -> y ; p et q -> contradiction ; p sans q -> z.
a = tms.ATMS()a.add_assumption('p'); a.add_assumption('q')for n in ('x', 'y', 'z'): a.add_node(n)a.add_justification(['p'], [], 'x')a.add_justification(['q', 'x'], [], 'y')a.add_justification(['p', 'q'], [], tms.ATMS.CONTRADICTION)a.add_justification(['p'], ['q'], 'z')labels = {n: sorted(tuple(sorted(e)) for e in nd.label) for n, nd in a.nodes.items()}for n, envs in labels.items():print(f'{n!r:6} : {envs}')assert labels['x'] == [('p',)] # x tient sous {p}assert labels['y'] == [] # {p,q} est nogood : y n'a plus rienassert labels['z'] == [('p',)] # blocage out : {q} non inclus dans {p}# Purge retroactive : y obtient {p,q} AVANT que la contradiction soit declaree.a2 = tms.ATMS()a2.add_assumption('p'); a2.add_assumption('q'); a2.add_node('y')a2.add_justification(['q', 'p'], [], 'y')a2.add_justification(['p', 'q'], [], tms.ATMS.CONTRADICTION)lab2 =sorted(tuple(sorted(e)) for e in a2.nodes['y'].label)print('purge retroactive, y :', lab2)assert lab2 == []
Lecture. Toute la table est une lecture d’explications simultanees : x tient sous {p} ; y sous aucun environnement (son seul soutien exige {p,q}, qui est nogood) ; z sous {p} (la clause out: q ne bloque pas {p}, et inversement {q} serait bloque par l’etiquette de… rien — c’est l’asymetrie mesuree du blocage out, gate 5). La purge est retroactive : meme declaree apres coup, la contradiction vide les etiquettes deja posees (gate 5b). Le JTMS aurait fallu N re-executions pour explorer ces N mondes ; l’ATMS les porte en un seul calcul — c’est le cout qu’il paie en memoire.
Quirk mesure et conserve (gate 5c) : le purge retire le nogood de l’etiquette du noeud contradiction lui-meme — apres purge, is_consistent({p,q}) repond True. Le nogood n’est pas memoire, il est consomme. C’est le comportement de la source a la tete mesuree ; on l’enseigne tel quel (honnêtete de distillation) avec son nom : perte documentee, pas silencieusement corrigee.
§5 — Le pont Dung <-> TMS, avec temoin negatif
Une attaque (a, b) de l’AF de Dung se lit dans le vocabulaire TMS : la validite de a soutient le rejet de b — une justification miroir in:[a] -> non-b. Le croisement ne traduit pas une semantique en l’autre : il les fait travailler ensemble. L’assertion ci-dessous est un temoin negatif : elle echouerait si le port divergeait de la source (les litteraux viennent de l’execution differentielle), si l’organe Phase A changeait son labeling, ou si le pont etait cable a l’envers. Toute re-execution de ce carnet re-verifie donc la fidelite de la distillation — c’est le garde-fou d’honnetete du grain.
af = arg.tweety_bird()labeling = arg.grounded_labeling(af)tp = tms.JTMS(strict=False)for u, v in af.attacks: tp.add_justification([f'arg{u}'], [], f'non-arg{v}') # attaque = rejet soutenufor i, lab in labeling.items():if lab =='in': tp.add_belief(f'arg{i}') tp.set_belief_validity(f'arg{i}', True)print('grounded (organe Phase A) :', labeling)print('rejets soutenus (TMS) :', {k: v for k, v insorted(tp.status_table().items()) if k.startswith('non-')})# TEMOIN NEGATIF (differential, tete EPITA 487210fb) : chaque attaquant accepte# au sens grounded soutient bien le rejet de sa cible ; aucun autre rejet n'est soutenu.for u, v in af.attacks:if labeling[u] =='in':assert tp.status_table()[f'non-arg{v}'] isTrue, f'pont casse : {u}->{v}'soutenus = {k for k, v in tp.status_table().items() if v isTrueand k.startswith('non-')}attendus = {f'non-arg{v}'for u, v in af.attacks if labeling[u] =='in'}assert soutenus == attendus, (soutenus, attendus)print('temoin negatif : OK —', len(soutenus), 'rejet(s) soutenu(s), exactement ceux du grounded.')
grounded (organe Phase A) : {0: 'in', 1: 'out', 2: 'in'}
rejets soutenus (TMS) : {'non-arg0': None, 'non-arg1': True}
temoin negatif : OK — 1 rejet(s) soutenu(s), exactement ceux du grounded.
Lecture. Le TMS soutient exactement les rejets dont l’attaquant est in au sens grounded — pas un de plus (la clause out ne fabrique rien ici), pas un de moins (la propagation suit les premisses posees). Les deux lectures se croisent : le grounded dit qui est acceptable, le TMS dit quel rejet est soutenu et pourquoi — et le Nixon diamond de l’exercice 3 montrera la limite du pont (deux arguments mutuellement attaquants : le grounded dit undec, et le pont TMS correspondant n’a aucune premisse a poser sans creer une boucle).
§6 — Exercices
Trois exercices pour s’approprier le substrat. Stubs a completer (convention C.1 : le notebook s’execute de bout en bout meme exercices non completes — return None, pas d’erreur volontaire). Les attendus sont mesurables : chaque stub nomme la verification qui jugera la reponse.
Methode recommandee (celle de la serie, cf. Phase B) : predire par ecrit avant de mesurer. Les tables des sections 3-5 n’ont pas ete devinees — elles ont ete predites puis confrontees au moteur, et c’est l’ecart entre les deux qui enseigne. Le Nixon diamond (exercice 1) est le cas ou la prediction naive est la plus fausse : la boucle d’attaques ne devient pas une boucle de justifications, et comprendre pourquoi est exactement l’objectif.
def exercice_1_nixon_jtms():"""Exercice 1 — Le Nixon diamond en JTMS. Construire un JTMS ou 'non-A' est soutenu par B et 'non-B' par A (miroir des attaques du Nixon diamond), poser A comme premisse, puis PREDIRE par ecrit la table avant de la mesurer. Etape 1 : ajouter les deux justifications miroir. Etape 2 : poser la premisse A. Etape 3 : comparer prediction et t.status_table(). Verification attendue : les croyances miroir ne forment PAS une boucle de justifications (non-A et non-B n'ont pas de justifications qui se soutiennent mutuellement) -- dites pourquoi en commentaire. """# TODO etudiantreturnNone# retourner la table mesureeprint('Exercice 1 a completer — prediction puis mesure.')resultat_1 = exercice_1_nixon_jtms()
Exercice 1 a completer — prediction puis mesure.
def exercice_2_atms_hypothese_r():"""Exercice 2 — Etendre l'ATMS d'une hypothese r. Reprendre l'instance de la section 4 (p, q, x, y, z, contradiction sur {p,q}) et ajouter : hypothese 'r', justification (in: [q, r], out: [], conclusion: 'w'). PREDIRE l'etiquette de w avant de mesurer. Etape 1 : construire l'instance complete (dans l'ordre de la section 4). Etape 2 : ajouter r et la justification de w. Etape 3 : lire a.get_environments('w'). Verification attendue : l'etiquette de w est {(q, r)} -- aucun nogood ne couvre {q, r}. Expliquer pourquoi le nogood {p,q} n'y change rien. """# TODO etudiantreturnNone# retourner l'ensemble des environnements de wprint('Exercice 2 a completer — prediction puis mesure.')resultat_2 = exercice_2_atms_hypothese_r()
Exercice 2 a completer — prediction puis mesure.
def exercice_3_pont_limite():"""Exercice 3 — La limite du pont Dung <-> TMS. Charger arg.nixon_diamond(), calculer son labeling grounded, construire le pont miroir (section 5) et tenter de poser UN argument comme premisse. Etape 1 : labeling de nixon_diamond (attendu : les deux 'undec'). Etape 2 : pont miroir des attaques. Etape 3 : mesurer ce que le TMS soutient quand aucune premisse n'est posee, puis quand une boucle de SOUTIEN (pas d'attaque) remplace le cycle -- que marque non_monotonic ? Verification attendue : le grounded dit 'undec' et le TMS, sans premisse, ne soutient aucun rejet -- les deux lectures s'accordent sur le refus de trancher. """# TODO etudiantreturnNone# retourner (labeling, table_du_pont)print('Exercice 3 a completer — la limite du pont.')resultat_3 = exercice_3_pont_limite()
Exercice 3 a completer — la limite du pont.
§7 — Conclusion
Ce carnet a distille la couche revision de l’argumentation : un moteur JTMS qui maintient un etat courant revisable (avec sa negation-as-failure mesuree et son refus de mesurer les boucles), un moteur ATMS qui porte tous les mondes d’hypotheses simultanement (avec sa purge retroactive et son nogood non persistant — quirk conserve, perte documentee), et un pont vers la semantique grounded de l’organe Phase A, verifie par temoin negatif. La fidelite n’est pas une impression : chaque valeur affichee est figee par execution differentielle contre la source EPITA (tete 487210fb), et les gates 1-6 des tests de l’organe (ict/tests/test_truth_maintenance.py) rejouent ces litteraux a chaque CI.
Sources et provenance : distillation-outil EPITA 2025 Argumentation, projet 1.4.1-JTMS (jtms.py, atms.py, corpus Beliefs/*.json), issues EPITA #1961 phase 4 — port declare dans ict/truth_maintenance.py. Organe Dung : ict.argumentation (Phase A, #7336). Instrument voisin : ICT-Argumentation-BeliefTrajectories (Phase B, #7742). Le verdict de distillation (fidele / perte documentee / perte par complaisance / divergence positive, par axe) est rendu sur le dashboard CoursIA, pas dans ce fichier.
Pour aller plus loin : Doyle 1979 (A truth maintenance system, AI 12) pour le JTMS original ; de Kleer 1986 (An assumption-based TMS, AI 28) pour l’ATMS ; Dung 1995 (On the acceptability of arguments) pour la semantique grounded — les trois references que la source EPITA operationnalise.