TweetyProject - Série de Notebooks Jupyter
Série complète de notebooks pour explorer TweetyProject, une bibliothèque Java pour l’intelligence artificielle symbolique. Le décompte exact des notebooks et leur maturité figurent dans le catalogue généré ci-dessous ; la série cible la version Tweety 1.30.
Série en quelques mots
À qui s’adresse cette série : étudiants en IA, chercheurs en argumentation computationnelle, développeurs intéressés par le raisonnement formel, et tout curieux souhaitant comprendre les bases mathématiques derrière le raisonnement explicite. Aucun prérequis en logique formelle n’est supposé : les concepts sont introduits progressivement, des opérateurs propositionnels de base jusqu’aux sémantiques d’argumentation les plus avancées.
Présentation
TweetyProject est une collection de bibliothèques Java couvrant plusieurs domaines :
- Logiques formelles : Propositionnelle, Premier ordre, Modale, Description, QBF
- Argumentation computationnelle : Dung, ASPIC+, DeLP, ABA, ADF
- Révision de croyances : AGM, Mesures d’incohérence, MUS/MCS
- Agents et dialogues : Multi-agents, Protocoles argumentatifs
- Préférences et vote : Ordres de préférence, Agrégation
Les notebooks utilisent deux implémentations pour exécuter TweetyProject, selon le langage d’apprentissage visé :
| Implémentation | Stack | Kernel | JVM requise ? | Notebooks |
|---|---|---|---|---|
| Python (originelle) | JPype (pont Java↔︎Python) | Python 3 | Oui (JDK téléchargé par le setup) | Tweety-1 à Tweety-11 (+ Tweety-02d-FOL-Lab-Lean labo FOL croisé, Tweety-02e-Preuves-Hilbert-Gentzen-Lean calculs de preuve Hilbert/LK, Tweety-5b-Lean-Argumentation companion Lean 4, Tweety-5d-Stable-Synthesis-Lean synthèse Z3→Lean, Tweety-5e-Propositional-Lab-Lean laboratoire propositionnel, Tweety-3b-Modal-Lab-Lean laboratoire modal et Tweety-02f-Modal-Zoo-Lean-Python sous-cube modal certifie — huit systemes et leur diagramme de Hasse) |
| C#/.NET (port natif) | IKVM 8.14 (bytecode Java→.NET) | .net-csharp |
Non (runtime IKVM pur .NET) | 18 notebooks *-Csharp (de Tweety-2-Basic-Logics-Csharp à Tweety-11-Causal-Csharp ; ex. 2b-Semantics, 3-Dung, 4-Aspic) |
Les deux implémentations couvrent les mêmes concepts fondamentaux (logique propositionnelle, sémantique des mondes possibles, logique du premier ordre, argumentation de Dung) ; le port C# les expose sans JVM, directement dans le runtime .NET, ce qui les rend exécutables côté .NET Interactive comme n’importe quel notebook C#. Les notebooks -Csharp vivent à côté de leurs homologues Python (pas dans un sous-dossier), pour faciliter la comparaison des deux stacks sur un même concept. Voir EPIC #4667.
Schéma de numérotation C# (clarification, cf. #5642, mandat #5081) : la série Tweety mêle deux conventions de nommage pour le port C# :
- Twin par numéro :
Tweety-N-<Topic>-Csharpjumelle le notebook PythonTweety-N-<Topic>(ex.Tweety-2-Basic-Logics+-Csharp,Tweety-5-Abstract-Argumentation+-Csharp). Le-Csharpapparaît à côté du Python pour la comparaison stack-à-stack. - Extension C#-only par suffixe lettre :
Tweety-2b-Semantics-Csharp,Tweety-2c-FOL-Csharp,Tweety-3-Conditional-Logics-Csharp,Tweety-3-ModalLogic-Csharp,Tweety-3-QBF-Csharpsont des extensions logiques pures sous le bloc 3 (Advanced Logics).
Cas Dung(3) / Aspic(4) — particularité : Tweety-3-Dung-Csharp et Tweety-4-Aspic-Csharp sont des extensions C#-only de l’argumentation computationnelle placées sous les numéros 3 (logique) et 4 (révision AGM) par proximité chronologique d’implémentation (la première vague du port C# a démarré avant la renumérotation narrative #5081). Ces deux notebooks seront migrés à terme vers Tweety-5c-Dung-Csharp (à côté de Tweety-5-Abstract-Argumentation) et Tweety-6c-Aspic-Csharp (à côté de Tweety-6-Structured-Argumentation) — voir #5642 pour la roadmap de renommage. En attendant, la coexistence (Dung sous 3, ASPIC+ sous 4) est documentée comme intentionnelle et pedagogiquement défendable (comparaison directe stack-à-stack entre Python et C# possible).
À l’heure des modèles statistiques et des LLMs, pourquoi étudier ces logiques symboliques ? Parce qu’elles apportent ce que l’apprentissage seul ne garantit pas : un raisonnement explicite, vérifiable et explicable. L’argumentation computationnelle (cadres de Dung, ASPIC+, ABA) modélise la façon dont des agents confrontent des arguments, gèrent les contradictions et aboutissent à des conclusions justifiées — avec des applications en raisonnement juridique, en aide à la décision, en négociation multi-agents, et de plus en plus comme couche de contrôle au-dessus des LLMs (détecter les incohérences, structurer un débat). La révision de croyances (AGM) formalise comment un agent rationnel met à jour ses connaissances face à une information nouvelle ou contradictoire. L’intérêt de TweetyProject est de réunir tous ces formalismes sous un même toit : on expérimente d’une logique à l’autre sans avoir à réimplémenter chaque solveur.
Symbolique vs. Statistique
Pour comprendre où se positionne cette série, voici une comparaison entre les approches symbolique et statistique de l’IA :
| Aspect | IA Symbolique (TweetyProject) | IA Statistique (ML/LLMs) |
|---|---|---|
| Représentation | Logiques formelles (PL, FOL, DL) | Vecteurs embeddings, poids neuronaux |
| Raisonnement | Déduction formelle, vérification | Inférence probabiliste, approximation |
| Vérifiabilité | Preuves mathématiques, solveurs | Benchmarks empiriques, statistiques |
| Explicabilité | Chaînes de raisonnement lisibles | Boîte noire, attention maps |
| Incohérence | Détection MUS/MCS, SAT solver | Gradient instability, divergence |
| Force | Garanties de correction | Adaptabilité, généralisation |
| Limite | Complexe à grande échelle | Manque de garanties formelles |
Cette série ne propose pas de choisir l’un ou l’autre, mais de comprendre les deux. L’intersection est d’ailleurs le front actif de la recherche : argumentation pour contrôler les LLMs, logiques neuronales, vérification formelle de modèles génératifs.
Vue d’ensemble
| Statistique | Valeur |
|---|---|
| Notebooks | 38 racine (13 Python + 7 Lean companion + 18 C#) + 1 probe |
| Cellules totales | 1170 (dont 446 code) — 38 racine + 1 probe |
| Durée estimée | ~6h (tutorat) |
| Kernel | Python 3 (JPype/Java) |
| Version Tweety | 1.30 recommandée |
| Solveurs externes | Clingo, SPASS, EProver, Z3, PySAT |
| JARs Java | 42 (39 modules Tweety 1.30 + 3 deps externes) |
Parcours d’apprentissage
flowchart LR
P1["<b>Phase 1</b><br/>Fondations<br/>logiques PL / FOL / DL / modale<br/>NB 1-3"]
P2["<b>Phase 2</b><br/>Révision de croyances<br/>AGM, MUS, MaxSAT<br/>NB 4"]
P3["<b>Phase 3</b><br/>Argumentation<br/>Dung + ASPIC/DeLP<br/>NB 5-6"]
P4["<b>Phase 4</b><br/>Frameworks avancés<br/>ADF, WAF, ranking, probabiliste<br/>NB 7a-7b"]
P5["<b>Phase 5</b><br/>Applications<br/>dialogues, vote, préférences<br/>NB 8-9"]
P1 --> P2 --> P3 --> P4 --> P5
%% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ton parfois plus fonce que le stroke (le stroke en couleur de texte rendrait infer illisible) : ne pas harmoniser
classDef core fill:#fff3cd,stroke:#856404,stroke-width:2px,color:#856404;
class P3 core;Le cœur de la série est la Phase 3 (argumentation, surlignée) — les fondations logiques et la révision de croyances y mènent, les frameworks avancés et les applications en découlent. Le détail de chaque phase suit.
Phase 1 : Fondations (Notebooks 1-3, ~1.5h)
La série débute avec le notebook 1 (Setup) qui configure toute l’environnement : téléchargement automatique du JDK Zulu, des 39 JARs des modules TweetyProject 1.30 (plus 3 dépendances externes), et des outils externes (Clingo pour ASP, SPASS pour la logique modale, EProver pour le premier ordre). Une fois la JVM initialisée via JPype, le notebook 2 plonge dans les logiques fondamentales : la logique propositionnelle avec les opérateurs booléens, la satisfaisabilité (SAT) via pySAT, et la logique du premier ordre avec la construction de signatures et le raisonnement avec EProver. Le notebook 3 étend ces fondations aux logiques de Description (DL) pour les ontologies, la logique modale (nécessité/possibilité) pour le raisonnement sur les mondes possibles, les formules booléennes quantifiées (QBF), et la logique conditionnelle pour le raisonnement defeasible. À l’issue de cette phase, vous maîtrisez les outils de base du raisonnement formel.
Phase 2 : Révision de Croyances (Notebook 4, ~45 min)
Ce notebook unique introduit la gestion de l’incohérence dans les systèmes intelligents. Plutôt que d’échouer face à des connaissances contradictoires, un système rationnel doit identifier les sources de conflit (MUS - Minimal Unsatisfiable Subsets), mesurer l’incohérence (scores et indices), et réélaborer ses croyances (révision AGM). Les outils pratiques incluent MaxSAT pour l’optimisation sous contraintes et le raisonnement multi-agents avec CrMas. C’est un pont entre les logiques pures et les systèmes multi-agents.
Phase 3 : Argumentation — De l’abstrait au structuré (Notebooks 5-6, ~2h)
Les notebooks 5 et 6 constituent le cœur de la série. Le notebook 5 introduit l’argumentation abstraite de Dung (1995) : un cadre où des arguments s’attaquent mutuellement sans regarder leur contenu interne. On y explore les sémantiques classiques (grounded, preferred, stable, semi-stable), la sémantique CF2 pour les cycles, et les nouveautés 1.30 (équivalence de frameworks, explications, raisonnement causal). Le notebook 6 monte d’un cran de granularité avec l’argumentation structurée : ASPIC+ (arguments construits à partir de règles defeasibles), DeLP (logique defeasible programmée), ABA (argumentation par hypothèse), et l’Answer Set Programming (ASP) via Clingo. La comparaison entre ces cadres montre que chacun offre un compromis différent entre expressivité et calculabilité.
Phase 4 : Frameworks avances et probabilistes (Notebooks 7a-7b, ~1h)
Le notebook 7a explore les extensions du cadre de Dung : ADF (Abstract Dialectical Frameworks, où les arguments peuvent avoir plusieurs preconditions), les frameworks bipolaires (support + attaque), les WAF (Weighted Argument Frameworks avec attaques pondérées), les SAF (Social Argumentation Frameworks), les SetAF (attaques collectives), et les frameworks étendus (attaques récursives sur des attaques). Le notebook 7b aborde deux axes différents : les sémantiques de classement (ranking) qui assignent un niveau de crédibilité à chaque argument plutôt que des extensions binaires, et l’argumentation probabiliste où les arguments portent des probabilités.
Phase 5 : Applications multi-agents (Notebooks 8-9, ~1h)
La série se conclut par deux notebooks applicatifs. Le notebook 8 modélise les dialogues argumentatifs entre agents : protocoles d’échange, jeux grounded, et loteries argumentatives. Le notebook 9 traite des préférences et de la théorie du vote : ordres de préférence, règles d’agrégation (Borda, Condorcet, Copeland), et leur connexion avec l’argumentation. C’est la passerelle vers la théorie des jeux et le choix social.
Parcours alternatifs
Parcours logique (focus fondations, ~2h)
Pour ceux qui souhaitent une base solide en logiques formelles avant l’argumentation :
- Setup (1) → Logiques de base (2) → Logiques avancées (3) → Révision (4)
- Puis choisir : Argumentation abstraite (5) pour la théorie pure, ou Applications (8-9) pour les cas d’usage
Parcours argumentation intensive (focus 5-7b, ~3.5h)
Pour les étudiants en argumentation computationnelle, aller droit au but :
- Setup rapide (1) : ne garder que la partie configuration JVM
- Logiques de base (2) : section PL uniquement, skip FOL si déjà connu
- Argumentation abstraite (5) : Dung + sémantiques
- Argumentation structurée (6) : ASPIC+ et DeLP
- Frameworks avancés (7a) : ADF + bipolarité
- Ranking et probabiliste (7b) : sémantiques de classement
Parcours applications (focus 8-9, ~1h)
Pour les praticiens intéressés par les applications multi-agents :
- Setup (1) + Logiques de base (2) : juste pour l’environnement
- Argumentation abstraite (5) : sémantiques de Dung essentielles
- Dialogues multi-agents (8) : protocoles et jeux grounded
- Préférences et vote (9) : théorie du vote et agrégation
Structure
La table ci-dessous distingue trois niveaux. Le parcours principal ne porte aucune lettre en ligne — il se lit de haut en bas. Les approfondissements vivent dans des sous-sections : les laboratoires croisés Python/Lean, les compagnons Lean natifs, et les jumeaux C#/.NET. La sous-série Argumentation a son propre parcours principal — Argumentum est un dépôt partenaire, ce README n’en est pas l’inventaire.
Parcours principal
Numéros nus uniquement, lisibles de haut en bas. Le compte et la maturité exacts vivent dans le bloc CATALOG-STATUS (haut de page).
| # | Notebook | Ce qu’on y apprend | Stack |
|---|---|---|---|
| 1 | Tweety-01-Setup-Python | Configuration JVM, JARs, solveurs externes | Python |
| 2 | Tweety-02-Basic-Logics-Python | Logique propositionnelle (SAT) et du premier ordre (FOL) | Python |
| 3 | Tweety-3-Advanced-Logics | DL, Modale, QBF, Conditionnelle | Python |
| 4 | Tweety-4-Belief-Revision | MUS, MaxSAT, Mesures d’incohérence, AGM | Python |
| 5 | Tweety-5-Abstract-Argumentation | Dung AF, sémantiques grounded/stable/CF2 | Python |
| 6 | Tweety-06-Structured-Argumentation-Python | ASPIC+, DeLP, ABA, ASP | Python |
| 7 | Tweety-07a-Extended-Frameworks-Python | ADF, Bipolar, WAF, SAF, SetAF, Extended | Python |
| 8 | Tweety-08-Agent-Dialogues-Python | Agents, dialogues argumentatifs, loteries | Python |
| 9 | Tweety-09-Preferences-Python | Préférences, théorie du vote | Python |
| 10 | Tweety-10-MLN | Markov Logic Networks (FOL pondérée) | Python |
| 11 | Tweety-11-Causal | do-calculus de Pearl, interventions, contrefactuels | Python |
| 12 | Tweety-12-Grounded-Via-TweetyProject | Bouclage de la sémantique grounded entre Python et Lean | Python |
Durée indicative du parcours léger : environ 13 h pour les notebooks racine Python. Le parcours s’arrête où vous voulez : le palier 5 (argumentation abstraite) ou le palier 6 (argumentation structurée) se suffisent à eux-mêmes pour qui ne vise que la modélisation du raisonnement.
Approfondissements
Une section par palier qui ouvre des lettres. Chaque lettre est facultative : on l’ouvre si le palier vous retient ou si vous préparez un pont vers un autre cours. Les laboratoires Python/Lean se lisent après avoir installé le noyau Lean (elan toolchain install stable, kernel Lean 4) ; les compagnons Lean natifs n’ont besoin que du noyau Lean.
Autour de 02 — sémantique propositionnelle, FOL, et laboratoires
| Lettre | Notebook | Ce que cette lettre ajoute |
|---|---|---|
| 02a | Tweety-02-Basic-Logics-CSharp | Jumeau C#/.NET du 02 (IKVM, port pilote #4792, premier pont Java→.NET de la série) |
| 02b | Tweety-02b-Semantics-CSharp | Sémantique propositionnelle .NET (mondes possibles) |
| 02c | Tweety-02c-FOL-CSharp | FOL porté .NET via IKVM 8.14 (tweetyproject.logics.fol.* réel) |
| 02d | Tweety-02d-FOL-Lab-Lean | Labo croisé (tranche B de l’EPIC #15066) : un même syllogisme exécuté par SimpleFolReasoner (six verdicts) et certifié par le noyau Lean sur le corpus FFL épinglé — conséquences quantifiées, contre-modèles finis exhibés ; la distinction FALSE ≠ « négation prouvée » y est mesurée |
| 02e | Tweety-02e-Preuves-Hilbert-Gentzen-Lean | Calculs de preuve (tranche D de l’EPIC #15066) : trois axiomes de Hilbert vérifiés par deux oracles réels, une preuve de Hilbert construite par chaînage avant (coût mesuré), puis le calcul des séquents LK — hauteur et taille d’un arbre avant/après élimination des coupures, le Hauptsatz étant invoqué comme théorème du noyau (Derivation.Canonical.constructiveHauptsatz, témoin IsCutFree) |
| 02f | Tweety-02f-Modal-Zoo-Lean-Python | Zoo modal certifié (tranche G de l’EPIC #15066) : huit systèmes normaux (K, KD, KT, KTB, K4, S4, KD45, S5) et l’ordre qui les relie. Les listes du module FormalLogic.ModalZoo (#17642) sont exportées par lake env lean (ModalZoo.toJson), l’ordre est recalculé en Python sur les seuls profils exportés, puis la carte est dessinée : 21 inclusions strictes sur 28 paires du cube, dont 11 arêtes de couverture, et 7 paires incomparables — chacune certifiée par le noyau |
Autour de 03 — logiques avancées : modal et laboratoire
| Lettre | Notebook | Ce que cette lettre ajoute |
|---|---|---|
| 03b | Tweety-3b-Modal-Lab-Lean | Labo modal croisé (tranche C de l’EPIC #15066) : schémas K/T/4/5 — syntaxe MlParser Tweety (bug SPASS #1334 documenté), balayage exhaustif des 512 cadres 3-mondes en Python (correspondances T/réflexif, 4/transitif, 5/euclidien mesurées en égalités exactes), certificats du kernel Lean sur le pont FormalLogic.ModalBridge (#17017) |
| 03c-DL | Tweety-3-Advanced-Logics-Csharp | DL/ML/QBF/CL .NET — DRAFT : conflits de noms DLL entre logics.ml + logics.cl + logics.qbf simultanés |
| 03c-CL | Tweety-3-Conditional-Logics-Csharp | Logique conditionnelle .NET (IKVM) — raisonneur cl réel |
| 03c-Dung | Tweety-3-Dung-Csharp | Argumentation de Dung .NET (IKVM, c.182 PR #5194) — NaiveDlReasoner |
| 03c-ML | Tweety-3-ModalLogic-Csharp | Logique modale .NET (IKVM) — MlReasoner réel |
| 03c-QBF | Tweety-3-QBF-Csharp | QBF .NET (IKVM, c.185 PR #5202) — solveur QBF réel |
Autour de 04 — belief revision et ASPIC+
| Lettre | Notebook | Ce que cette lettre ajoute |
|---|---|---|
| 04c-BR | Tweety-4-Belief-Revision-Csharp | Belief Revision .NET (IKVM) : Revision/MUSMaxSAT réels |
| 04c-Aspic | Tweety-4-Aspic-Csharp | ASPIC+ .NET (IKVM) — AspicArgumentation réel |
Autour de 05 — argumentation abstraite et compagnons Lean
| Lettre | Notebook | Ce que cette lettre ajoute |
|---|---|---|
| 05b | Tweety-5b-Lean-Argumentation | Compagnon natif (kernel Lean) : preuve formelle 0-sorry de Dung dans le lake argumentation_lean (grounded = point fixe Knaster–Tarski), #check + #print axioms in-kernel (UNLOCK c.127, jonction Mathlib #2611) |
| 05c | Tweety-5-Abstract-Argumentation-Csharp | Twin C# Dung AF from-scratch (BCL .NET, pas IKVM/JVM) : fonction caractéristique, acceptabilité, ensembles admissibles/complets, sémantiques grounded (plus petit point fixe) / stable / preferred, labeling 3 valeurs (in/out/undec), génération aléatoire, 3 exercices |
| 05d | Tweety-5d-Stable-Synthesis-Lean | Synthèse certifiée d’extensions stables (Loi II #12205, variante -c, #13597) : spécification → Z3 (générateur ≠ vérificateur) → témoin {1, 2, 5} → certificat Lean by decide dans le lake argumentation_lean (module Argumentation.Synthesis + sibling _en, i18n #4980) ; cas UNSAT du 3-cycle certifié (afB_no_stable) |
| 05e | Tweety-5e-Propositional-Lab-Lean | Compagnon transversal (tranche A de l’EPIC #15066) : trois formules-témoins (SYL valide, ORB satisfiable non valide, CONTR insatisfiable) traversent trois lectures — Tweety via JPype (verdicts et contre-modèles calculés), recomptage Python indépendant des 8 mondes du fragment {a, b, c}, certification du kernel Lean natif sur Foundation (FFL) au commit épinglé ; la même chaîne de formule est sérialisée pour les deux moteurs (SOTA, aucune réimplémentation jouet) |
Autour de 06 — argumentation structurée et jumeau C
| Lettre | Notebook | Ce que cette lettre ajoute |
|---|---|---|
| 06c | Tweety-06-Structured-Argumentation-CSharp | Twin C# ASPIC+ from-scratch (BCL, pas IKVM ; DeLP/ABA/ASP conceptuel) |
Autour de 07 — cadres étendus et probabilistes
Le palier 07 est porté par le 07a (Python) et son jumeau 07ac (C#) ; le 07b (probabiliste) en est l’approfondissement.
| Lettre | Notebook | Ce que cette lettre ajoute |
|---|---|---|
| 07ac | Tweety-07a-Extended-Frameworks-CSharp | Twin C# hybride : ADF/SetAF/EAF/VAF from-scratch (BCL, Kleene 3-valued) + tranche 2 lib Tweety réelle via IKVM (DLL shade 7a versionnée à la racine, rebuildable via dotnet-build/rebuild-7a.sh ; #4956) |
| 07b | Tweety-07b-Ranking-Probabilistic-Python | Sémantiques de classement (ranking) et argumentation probabiliste |
| 07bc | Tweety-07b-Ranking-Probabilistic-CSharp | Jumeau C# du 07b (IKVM, c.179 PR #5231) — Ranking, SubgraphProbability réels |
Autour de 08 et 09 — applications multi-agents
| Lettre | Notebook | Ce que cette lettre ajoute |
|---|---|---|
| 08c | Tweety-08-Agent-Dialogues-CSharp | Twin C# dialogues argumentatifs from-scratch (BCL .NET, pas IKVM/JVM ; Dung AF + agents + protocole Claim/Argue/Concede/Retract + loterie argumentative Monte-Carlo) |
| 09c | Tweety-09-Preferences-CSharp | Préférences .NET (IKVM, c.180 PR #5268) |
Autour de 10 et 11 — synthèse
| Lettre | Notebook | Ce que cette lettre ajoute |
|---|---|---|
| 10c | Tweety-10-MLN-Csharp | MLN porté .NET (IKVM, c.188 PR #5209) — MarkovLogicNetwork, vrais appels |
| 11c | Tweety-11-Causal-Csharp | Twin C# moteur causal booléen from-scratch .NET : do-operator, contrefactuels par mondes jumeaux |
Sous-série Argumentation — Argumentum
Les notebooks 5 et 6 sont la couche Tweety de la sous-série Argumentation : ils portent les fondations de Dung et d’ASPIC+. Argumentum, le partenaire agentique, vit dans un dépôt externe et applique ces sémantiques à des textes. Voir Argument_Analysis pour la série partenaire, et le sous-module pour le code source de l’agent.
Durée totale indicative : ~13 h (Python) + ~10 h (C#/.NET). Le tableau ci-dessus couvre les notebooks principaux (12 Python + 18 C#/.NET + 7 Lean companion) ; voir aussi _probes/Tweety-IKVM-Init-Probe.ipynb (BETA smoke-test IKVM) et argumentation_lean/ (lake Lean 4, toolchain v4.32.1 depuis #11587, avec les fichiers .lean du dossier Argumentation/ — les modules FR : Basic, Characteristic, Extensions, Fundamental, Grounded, Synthesis + leurs siblings _en i18n #4980).
En quoi chaque notebook est unique
Chaque notebook introduit un concept ou cadre théorique spécifique. Le tableau ci-dessous résume en une ligne l’apport pédagogique de chacun — couvrant les notebooks principaux (12 Python + 18 C#/.NET + 7 Lean companion) :
| # | Notebook | Concept clé enseigné |
|---|---|---|
| 1 | Setup | Boucle configuration : JVM → JPype → JARs → solveurs externes |
| 2 | Basic Logics | SAT solving en pratique (pySAT) + formalisme FOL avec EProver |
| 2a | Basic Logics (C#, pilote) | Logique propositionnelle .NET — port pilote IKVM (#4792), premier pont Java→.NET de la série |
| 2b | Semantics (C#) | Sémantique propositionnelle .NET (mondes possibles) — port IKVM 8.14 |
| 2c | Basic Logics (C#) | FOL porté .NET via IKVM 8.14 : tweetyproject.logics.fol.* réel |
| 2d | FOL Lab (Python+Lean) | Un syllogisme, deux moteurs : SimpleFolReasoner exécute six verdicts, le noyau Lean certifie conséquences (théorèmes) et non-conséquences (contre-modèles finis) — FALSE n’est pas « négation prouvée » |
| 2e | Preuves Hilbert/LK (Python+Lean) | Deux calculs de preuve mesurés : Hilbert (axiomes + MP, recherche par chaînage avant, coût en instances/MP) et séquents LK (hauteur/taille d’arbre avant/après élimination des coupures, Hauptsatz = théorème du noyau) |
| 2f | Zoo modal (Python+Lean) | Huit systèmes modaux et leur ordre partiel : les données du module exportées par lake env lean, l’ordre recalculé sur les profils, puis la carte — 11 arêtes de couverture contre 7 paires incomparables ; « incomparable » n’est ni « un peu plus faible » ni « on ne sait pas » |
| 3 | Advanced Logics | Ontologies OWL (DL) + raisonnement modale (SPASS) + QBF |
| 3b | Modal Lab (Python+Lean) | Théorie de la correspondance mesurée : énumération exhaustive 512 cadres ↔︎ contre-modèles kernel-vérifiés (pont ModalBridge) |
| 3c-DL | Advanced Logics (C#) | DL/ML/QBF/CL .NET — DRAFT : conflits de noms DLL entre logics.ml + logics.cl + logics.qbf simultanés |
| 3c-CL | Conditional Logics (C#) | Logique conditionnelle .NET (IKVM) — raisonneur cl réel |
| 3c-Dung | Dung (C#) | Argumentation de Dung .NET (IKVM, c.182 PR #5194) — NaiveDlReasoner |
| 3c-ML | Modal Logic (C#) | Logique modale .NET (IKVM) — MlReasoner réel |
| 3c-QBF | QBF (C#) | QBF .NET (IKVM, c.185 PR #5202) — solveur QBF réel |
| 4 | Belief Revision | Identification de conflits (MUS) + révision AGM + MaxSAT |
| 4c-BR | Belief Revision (C#) | Belief Revision .NET (IKVM) : Revision/MUSMaxSAT réels, BETA |
| 4c-Aspic | Aspic (C#) | ASPIC+ .NET (IKVM) — AspicArgumentation réel |
| 5 | Abstract Argumentation | Sémantiques de Dung (grounded/stable/CF2) + frameworks aléatoires |
| 5b | Lean Argumentation | Companion natif (kernel Lean) : preuve formelle 0-sorry de Dung dans le lake argumentation_lean, BETA |
| 5c | Abstract Argumentation (C#) | Dung AF from-scratch BCL .NET (sans IKVM/JVM) : sémantiques grounded/stable/preferred, labeling 3 valeurs |
| 5d | Stable Synthesis (Lean) | Synthèse certifiée d’extensions stables : spécification → générateur Z3 → témoin → certificat Lean by decide dans le lake argumentation_lean (module Argumentation.Synthesis), cas UNSAT du 3-cycle certifié |
| 5e | Propositional Lab (Lean) | Trois lectures d’une même formule — Tweety (verdicts et contre-modèles calculés), recomptage Python des 8 mondes, certification Lean sur Foundation (FFL) au commit épinglé ; théâtre des trois verdicts valid / satisfiable non valide / insatisfiable |
| 6 | Structured Argumentation | Comparaison ASPIC+/DeLP/ABA/ASP — le cadre idéal selon le domaine |
| 6c | Structured Argumentation (C#) | ASPIC+ from-scratch BCL .NET (sans IKVM) — DeLP/ABA/ASP en contrepoint conceptuel |
| 7a | Extended Frameworks | Au-delà de Dung : ADF, bipolarité, attaques pondérées et collectives |
| 7ac | Extended Frameworks (C#) | Hybride : ADF/SetAF/EAF/VAF from-scratch BCL .NET (logique de Kleene 3 valeurs) + tranche 2 Dung/Weighted/Social/ADF via la lib Tweety reelle (IKVM, DLL shade 7a versionnee) |
| 7b | Ranking & Probabilistic | Classement graduel des arguments + incertitude sur les arguments |
| 7bc | Ranking & Probabilistic (C#) | Ranking/Probabiliste .NET (IKVM) — Ranking, SubgraphProbability réels |
| 8 | Agent Dialogues | Protocoles d’échange entre agents + négociation argumentative |
| 8c | Agent Dialogues (C#) | Dialogues argumentatifs from-scratch BCL .NET : protocole Claim/Argue/Concede/Retract + loterie Monte-Carlo |
| 9 | Preferences | Agrégation de préférences (Borda, Condorcet) + théorie du vote |
| 9c | Preferences (C#) | Préférences .NET (IKVM, EPIC #4667 PR #5268) |
| 10 | MLN | Pont symbolique/statistique : FOL + poids, marginales, exceptions (pingouin) |
| 10c | MLN (C#) | MLN porté .NET (IKVM) : MarkovLogicNetwork, vrais appels |
| 11 | Causalité | do-calculus de Pearl : intervention do(X) vs observation, contrefactuels |
| 11c | Causalité (C#) | Moteur causal booléen from-scratch .NET : do-operator, contrefactuels par mondes jumeaux |
Le pont symbolique/statistique (notebook 10 — MLN)
Le notebook 10 introduit les Markov Logic Networks, qui font varier le « degré de logique » d’une formule via son poids w. À une extrémité (w → ∞), on retrouve la logique classique (un seul monde violant rend la base inconsistante) ; à l’autre (w = 0), la statistique pure (tous les mondes équiprobables). Le paradoxe du pingouin illustre comment ce spectre résout des cas qu’aucune des deux extrêmes ne sait traiter seule :
flowchart LR
LOGIC["<b>Logique classique</b><br/>FOL stricte<br/><i>w → ∞ (règle dure)</i><br/>un seul monde violant = ⊥"]
MLN["<b>Markov Logic Network</b><br/>P(world) ∝ exp(Σ wᵢ · nᵢ)<br/>chaque formule FOL = une contrainte <i>souple</i>"]
STAT["<b>Statistique pure</b><br/>mondes équiprobables<br/><i>w = 0 (aucune contrainte)</i>"]
LOGIC -.->|"poids croissant"| MLN
MLN -.->|"poids décroissant"| STAT
PENG(["<b>Paradoxe du pingouin</b> — discrimine les deux extrêmes<br/>Flies(tweety) = 0.00 : l'exception stricte « pingouin ⇒ ¬vole » l'emporte<br/>Flies(robin) = 0.79 : la règle pondérée « oiseau ⇒ vole » seule, sans exception"])
MLN --> PENGL’échelle causale de Pearl (notebook 11 — Causalité)
Le notebook 11 monte d’un niveau par rapport aux approches probabilistes : il distingue corrélation et causalité grâce à l’opérateur do(X). Judea Pearl formalise cette distinction par une échelle à trois niveaux, chaque saut étant inaccessible au niveau inférieur. Le scénario du baromètre illustre le saut crucial entre les niveaux 1 et 2 : observer la baisse du baromètre prédit la pluie (corrélation via l’orage), mais forcer le baromètre à baisser ne fait pas pleuvoir (pas de causalité) :
flowchart TD
L1["<b>Niveau 1 — Association</b><br/>observe(X) → Y<br/>P(rain | drops) = <b>True</b><br/><i>corrélation : drops et rain coïncident via le confondeur storm</i>"]
L2["<b>Niveau 2 — Intervention</b><br/>do(X) → Y<br/>P(rain | do(drops)) = <b>False</b><br/><i>l'opérateur do ROMPT l'équation storm → drops ; drops ne porte plus d'info sur rain</i>"]
L3["<b>Niveau 3 — Contrefactuel</b><br/>« si X avait été différent, Y aurait-il eu lieu ? »<br/>observe(wet) ∧ ¬sprinkler → wet = <b>True</b><br/><i>twin model : rain aurait suffi à mouiller l'herbe</i>"]
L1 -->|"saut inaccessible à la statistique seule"| L2
L2 -->|"saut inaccessible à l'intervention seule"| L3La signature du do-calculus — P(rain | drops) ≠ P(rain | do(drops)) — est exactement ce que la logique classique (notebooks 1-4) et les MLN (notebook 10) restent incapables d’exprimer : ils ne connaissent que l’association.
Ponts causaux — le do-calculus au-delà du symbolique
Tweety raisonne sur le do-calculus en logique propositionnelle : do(X) y est qualitatif — un atome forcé, un SCM réécrit, une réponse vrai/faux. C’est idéal pour voir la différence entre observe et do sans nombres, mais Tweety ne chiffre pas un effet causal ni ne lève quantitativement un paradoxe de Simpson. Les séries probabilistes du dépôt reprennent exactement ce notebook avec des distributions :
- Infer-5-Causal-Inference — le jumeau distributionnel par message passing :
P(Y|do(X))calculé par mutilation de graphe en Infer.NET (EP/VMP), ajustements backdoor / front-door, paradoxe de Simpson résolu numériquement. - PyMC-05-Causal-Inference — la version MCMC avec l’opérateur natif
pm.doet le contrefactuel par abduction. - ICT-05-CausalEmergence-Python — le même
domonte d’un cran : à quelle échelle un système fait-il le plus de travail causal ?
Vue d’ensemble des quatre paradigmes : le README IIT, section « Ponts causaux : le do-calculus de Pearl à travers les paradigmes ».
Concepts clés
| Concept | Description |
|---|---|
| Logique Propositionnelle | Operateurs booléens, DNF, satisfaisabilité (SAT) |
| Logique du Premier Ordre | Quantificateurs (∀, ∃), prédicats, fonctions |
| Logique de Description | Ontologies, TBox/ABox, sous-typage, OWL |
| Logique Modale | Nécessité (□) et possibilité (◇), mondes possibles |
| Argumentation de Dung | Frameworks abstraits, attaques, sémantiques (grounded, stable) |
| Argumentation structurée | Arguments construits à partir de prémisses et règles |
| Révision AGM | Mise à jour rationnelle de croyances face à l’information contradictoire |
| MUS/MCS | Sous-ensembles insatisfaisables/maximaux — identifier les conflits |
| Answer Set Programming | Programmation par modèles (ASP) via Clingo |
| Agrégation de préférences | Borda, Condorcet, Copeland — combiner des opinions |
Domaines d’application
| Domaine | Notebooks | Exemple concret |
|---|---|---|
| Juridique | 5, 6, 8 | Argumentation légale, débats en cour, preuve par argument |
| Aide à la décision | 4, 9 | Diagnostic médical, planification de ressources, vote |
| Multi-agents | 8 | Négociation automatique, protocoles de dialogue |
| Ontologies | 3 | Représentations de connaissances, OWL, Web sémantique |
| Vérification formelle | 2, 3, 4 | SAT/SMT solving, proof checking, model checking |
| LLM control | 5, 6, 7b | Détection d’incohérences, structuration de débats, argumentation probabiliste |
Exemples concrets
Derrière chaque cadre de la série se cache une application réelle ou un problème de recherche actif :
- L’argumentation de Dung (notebook 5) est le fondement mathématique de nombreux systèmes d’aide à la décision juridique : des arguments se confrontent, les sémantiques déterminent quels arguments sont “acceptables”, et le résultat guide la conclusion. C’est aussi la base des frameworks d’explicabilité des LLMs — détecter les incohérences entre réponses d’un modèle.
- ASPIC+ et DeLP (notebook 6) modélisent des débats où les arguments ont une structure interne : prémisses, règles defeasibles, et priorités. Applications en aide à la décision médicale, en gestion de conflits de règles, et en vérification de contrats.
- La révision de croyances AGM (notebook 4) formalise comment un système rationnel met à jour ses connaissances quand une information contradictoire arrive. Applications en intégration de données, diagnostic de bases de connaissance, et fusion de sources d’information.
- Les frameworks étendus (notebook 7a) généralisent Dung pour capturer des situations réelles où des arguments ont plusieurs preconditions (ADF), où des attaques ont des poids variés (WAF), ou des groupes d’arguments attaquent collectivement (SetAF).
- La théorie du vote (notebook 9) est au cœur des systèmes de recommandation collective, de l’agrégation de préférences en intelligence artificielle, et des mécanismes d’incitation (mechanism design).
Un framework de Dung, visualisé
L’argumentation abstraite de Dung (notebook 5) se réduit à un graphe orienté : des nœuds (les arguments) et des flèches (les attaques). La question n’est pas « l’argument est-il vrai ? » mais « survive-t-il aux attaques ? » — c’est ce que calculent les sémantiques. Exemple minimal :
flowchart LR
C(["<b>C</b>"]) -->|"attaque"| B["<b>B</b>"]
B -->|"attaque"| A["<b>A</b>"]
classDef acc fill:#d4edda,stroke:#28a745,stroke-width:2px,color:#155724;
classDef rej fill:#f8d7da,stroke:#dc3545,stroke-width:2px,color:#721c24;
class C acc;
class A acc;
class B rej;Extension grounded : C n’est attaqué par personne → accepté ; B est attaqué par l’accepté C → rejeté ; A n’est attaqué que par le rejeté B → accepté. D’où {A, C}. La règle se tient en une phrase : un argument est acceptable si tous ses attaquants sont eux-mêmes défaits. Les sémantiques preferred/stable, les cycles (CF2) et le raisonnement causal du notebook 5 raffinent ce même calcul.
Quick Start
# 1. Installer les packages Python
pip install jpype1 requests tqdm clingo z3-solver python-sat
# 2. Ouvrir le notebook de setup (auto-télécharge JDK + JARs)
jupyter notebook Tweety-01-Setup-Python.ipynb
# 3. Exécuter toutes les cellules, puis passer à Tweety-2JDK 17 et les 42 JARs (39 modules TweetyProject 1.30 + 3 dépendances externes : args4j, commons-math, sat4j) sont téléchargés automatiquement par le notebook de setup. Aucune installation système requise.
Prérequis
Niveau mathématique attendu
Cette série suppose une maîtrise de base en logique et raisonnement :
| Concept | Utilisation dans la série | Notes de révision |
|---|---|---|
| Logique propositionnelle (ET, OU, NON, →) | Notebook 2 (PL), 5+ (argumentation) | Tables de vérité, DNF/CNF, satisfaisabilité |
| Logique du premier ordre (quantificateurs) | Notebook 2 (FOL), 3 (DL) | ∀, ∃, variables, prédicats |
| Graphes (nœuds, arêtes) | Notebook 5 (Dung AF), 7a (SetAF) | Chemins, cycles, orientés |
| Ensembles (inclusion, union, intersection) | Partout (extensions, bases) | Ensembles finis, parties |
| Raisonnement par récurrence | Notebook 3 (DL), 5 (sémantiques) | Principe de récurrence bien-fondée |
Inutile de maîtriser : théorie de la preuve formelle, complexité computationnelle avancée (la complexité des sémantiques de Dung est expliquée en contexte). Les concepts logiques sont introduits progressivement dans chaque notebook.
Prérequis techniques
Python et dépendances
pip install jpype1 requests tqdm clingo z3-solver python-satJava/JVM
- JDK 17+ — telechargé automatiquement (Zulu) par le notebook de setup
- JPype — bridge Python ↔︎ Java (charge automatiquement les JARs)
Outils externes (optionnels mais recommandés)
| Outil | Usage | Installation |
|---|---|---|
| Clingo 5.4+ | ASP (Answer Set Programming) | download_tweety_tools.py --clingo |
| SPASS | Logique modale | Binaire inclus ou auto-download Linux |
| EProver | FOL haute performance | Installation manuelle ou dossier inclus |
| Z3 | SMT solver, MARCO | pip install z3-solver |
| PySAT | SAT/MaxSAT moderne | pip install python-sat |
Installation
Packages Python requis
pip install jpype1 requests tqdm clingo z3-solver python-satVérification de l’environnement
# Lancer le notebook de setup
jupyter notebook Tweety-01-Setup-Python.ipynb
# Exécuter toutes les cellules — il télécharge JDK, JARs, outils externes
# Ou utiliser le script de validation
cd scripts
python verify_all_tweety.py --quickJDK 17 et les 42 JARs (39 modules TweetyProject 1.30 + 3 dépendances externes : args4j, commons-math, sat4j) sont téléchargés automatiquement par le notebook de setup. Aucune installation système requise.
Architecture
Tweety/
├── Tweety-01-Setup-Python.ipynb # Configuration JVM/JPype
├── Tweety-02-Basic-Logics-Python.ipynb # PL + FOL
├── Tweety-02-Basic-Logics-CSharp.ipynb # Logique propositionnelle .NET (IKVM, PROD)
├── Tweety-02b-Semantics-CSharp.ipynb # Sémantique propositionnelle .NET (IKVM, BETA)
├── Tweety-02c-FOL-CSharp.ipynb # FOL .NET (IKVM, BETA)
├── Tweety-02d-FOL-Lab-Lean.ipynb # Labo FOL croisé Tweety/Lean (tranche B #15066)
├── Tweety-02e-Preuves-Hilbert-Gentzen-Lean.ipynb # Calculs de preuve Hilbert/LK (tranche D #15066)
├── Tweety-02f-Modal-Zoo-Lean-Python.ipynb # Zoo modal certifie : 8 systemes, Hasse (tranche G #15066)
├── Tweety-3-Advanced-Logics.ipynb # DL, ML, QBF, CL
├── Tweety-3b-Modal-Lab-Lean.ipynb # Labo modal croisé Kripke/Lean (tranche C #15066)
├── Tweety-3-Advanced-Logics-Csharp.ipynb # DL/ML/QBF/CL .NET (DRAFT — conflits DLL)
├── Tweety-3-Conditional-Logics-Csharp.ipynb # Logique conditionnelle .NET (IKVM, PROD)
├── Tweety-3-Dung-Csharp.ipynb # Argumentation de Dung .NET (IKVM, PROD)
├── Tweety-3-ModalLogic-Csharp.ipynb # Logique modale .NET (IKVM, PROD)
├── Tweety-3-QBF-Csharp.ipynb # QBF .NET (IKVM, PROD)
├── Tweety-4-Belief-Revision.ipynb # Révision de croyances
├── Tweety-4-Belief-Revision-Csharp.ipynb # Belief Revision .NET (IKVM, BETA)
├── Tweety-4-Aspic-Csharp.ipynb # ASPIC+ .NET (IKVM, BETA)
├── Tweety-5-Abstract-Argumentation.ipynb # Dung, sémantiques, CF2
├── Tweety-5-Abstract-Argumentation-Csharp.ipynb # Twin C# Dung AF from-scratch (BCL, BETA)
├── Tweety-5b-Lean-Argumentation.ipynb # Companion kernel Lean 4
├── Tweety-5d-Stable-Synthesis-Lean.ipynb # Synthèse certifiée Z3→Lean (Loi II #12205)
├── Tweety-5e-Propositional-Lab-Lean.ipynb # Laboratoire propositionnel Tweety/Lean (tranche A #15066)
├── Tweety-06-Structured-Argumentation-Python.ipynb # ASPIC+, DeLP, ABA, ASP
├── Tweety-06-Structured-Argumentation-CSharp.ipynb # Twin C# ASPIC+ from-scratch (BCL, PROD)
├── Tweety-07a-Extended-Frameworks-Python.ipynb # ADF, Bipolar, WAF, SAF
├── Tweety-07a-Extended-Frameworks-CSharp.ipynb # Twin C# ADF/SetAF/EAF/VAF from-scratch (BCL, PROD)
├── Tweety-07b-Ranking-Probabilistic-Python.ipynb # Ranking Semantics
├── Tweety-07b-Ranking-Probabilistic-CSharp.ipynb # Ranking/Probabiliste .NET (IKVM, PROD)
├── Tweety-08-Agent-Dialogues-Python.ipynb # Agents, dialogues, loteries
├── Tweety-08-Agent-Dialogues-CSharp.ipynb # Twin C# dialogues from-scratch (BCL, PROD)
├── Tweety-09-Preferences-Python.ipynb # Préférences, vote
├── Tweety-09-Preferences-CSharp.ipynb # Préférences .NET (IKVM, PROD)
├── Tweety-10-MLN.ipynb # Markov Logic Networks
├── Tweety-10-MLN-Csharp.ipynb # MLN .NET (IKVM, PROD)
├── Tweety-11-Causal.ipynb # do-calculus Pearl
├── Tweety-11-Causal-Csharp.ipynb # Twin C# moteur causal from-scratch (BCL, PROD)
├── tweety_init.py # Module d'initialisation JPype/JVM
├── requirements.txt # Dépendances Python (JPype1, etc.)
├── org.tweetyproject.tweety-*.dll # 19 assemblages .NET (shades IKVM, EPIC #4667)
├── dotnet-build/ # Build Maven/.csproj des shades IKVM (EPIC #4667)
├── libs/ # JARs Tweety (42 : 39 modules 1.30 + 3 deps) — téléchargé
├── jdk-17-portable/ # JDK Zulu — téléchargé auto par le setup
├── ext_tools/ # Solveurs externes (Clingo, SPASS, EProver) — téléchargé
├── resources/ # Fichiers d'exemples — téléchargé
├── scripts/
│ ├── download_tweety_tools.py # Téléchargement des dépendances
│ ├── verify_all_tweety.py # Validation
│ ├── validate_syntax.py # Validation syntaxe Python
│ ├── sat_calibration.py # Calibration SAT
│ ├── sat_comparison_demo.py # Démo comparative SAT
│ ├── test_*.py # 4 tests unitaires (sat_calibration, sat_comparison_demo, validate_syntax, verify_tweety_iopub)
│ └── _archive/ # Scripts archivés (reorganize_tweety.py)
├── _probes/ # Smoke-tests (1 nb : Tweety-IKVM-Init-Probe)
├── argumentation_lean/ # Lake Lean 4 (6 modules .lean + 6 siblings _en, i18n #4980)
└── README.md # Ce fichierNote : les dossiers
libs/,jdk-17-portable/,ext_tools/etresources/sont des répertoires d’exécution (non suivis par Git, téléchargés automatiquement parTweety-01-Setup-Python.ipynbouscripts/download_tweety_tools.py). L’ancien dossiertemplates student/n’existe plus dans cette partition.scripts/contient 5 scripts.pyau premier niveau (download_tweety_tools.py,verify_all_tweety.py,validate_syntax.py,sat_calibration.py,sat_comparison_demo.py), 4 teststest_*.pyet unREADME.md, plus un sous-dossier_archive/(qui contientreorganize_tweety.py, déplacé depuis le premier niveau — plus de doublon). Le dossier_output/n’est pas présent dans cette partition (les traces Papermill ne sont pas conservées). Audit §E whole-file gate 2026-07-15, re-audit 2026-08-15, re-audit fichier-entier 2026-09-25 (comptes de notebooks, cellules et durées re-mesurés sur disque — périmètre et résidus déclarés dans l’entrée de changelog).
Outils Externes
Script de téléchargement automatisé
Un script autonome est disponible pour télécharger toutes les dépendances :
cd MyIA.AI.Notebooks/SymbolicAI/Tweety
# Télécharger tout (JARs, ressources, outils)
python scripts/download_tweety_tools.py --all
# Télécharger uniquement les JARs
python scripts/download_tweety_tools.py --jars
# Télécharger uniquement les ressources
python scripts/download_tweety_tools.py --resources
# Télécharger Clingo (ASP solver)
python scripts/download_tweety_tools.py --clingo
# Voir toutes les options
python scripts/download_tweety_tools.py --helpListe des dépendances
| Outil | Usage | Téléchargement Auto | Versionné Git |
|---|---|---|---|
| Clingo | ASP (Answer Set Programming) | Oui (Win/Linux) | Oui (binaire Windows) |
| SPASS | Logique Modale | Oui (Linux) | Oui (binaire + docs Windows) |
| EProver | FOL haute performance | Non | Oui (installation complète) |
| Z3 | SMT solver, MARCO | pip install z3-solver |
N/A (package Python) |
| PySAT | SAT/MaxSAT moderne | pip install python-sat |
N/A (package Python) |
| Native SAT | Bibliothèques SAT JNI | Oui | Oui (DLLs Minisat, Lingeling) |
| JDK 17 | JVM pour JPype | Oui (Zulu) | Non (trop volumineux) |
| JARs Tweety | Bibliothèques Java | Oui (Maven Central) | Non (trop volumineux) |
| Resources | Fichiers exemples | Oui (GitHub) | Non (fichiers de données) |
Notes d’installation
Clingo
- Télécharge automatiquement pour Windows et Linux
- Version 5.4.0 depuis GitHub releases (potassco/clingo)
- Si déjà installé dans le PATH, utilise la version système
SPASS (Windows)
Le téléchargement automatique n’est PAS disponible sur Windows (l’installeur ne peut pas être automatisé)
Deux options :
- Utiliser le binaire déjà inclus dans le dépôt Git (
ext_tools/spass/SPASS.exe) - Installation manuelle :
- Télécharger depuis https://www.spass-prover.org/download/binaries/
- Exécuter l’installeur
spass30windows.exe - Copier
SPASS.exeet le dossierSPASS-3.0/versext_tools/spass/
- Utiliser le binaire déjà inclus dans le dépôt Git (
SPASS (Linux)
- Télécharge automatiquement (version 64-bit ou 32-bit selon l’architecture)
EProver
- Doit être installé manuellement : https://eprover.org/
- L’installation complète est déjà incluse dans
../ext_tools/EProver/ - Contient tous les utilitaires : eprover, eground, enormalizer, etc.
Bibliothèques natives SAT
- DLLs Windows (Minisat, Lingeling, Picosat) pour Tweety JNI
- Téléchargeables automatiquement ou déjà incluses dans
libs/native/
Limitations Connues
Limitations constatées à l’origine sous Tweety 1.28/1.29 et toujours documentées dans les notebooks courants (série 1.30 — le notebook 4 cite les changements de package 1.28 pour CrMas, le notebook 5 le ClassCastException) :
| Limitation | Impact | Contournement |
|---|---|---|
| CrMas/InformationObject | Section révision multi-agents échoue | API refactorisée, classe supprimée |
| SimpleMlReasoner | Bloque indéfiniment | Utiliser SPASS externe |
| AF Learning | ClassCastException | Bug interne, section désactivée |
| ADF natif SAT | Raisonnement ADF incomplet | Nécessite solveur SAT natif (non JPype) |
| FOL avec égalité | Heap space sur grandes requêtes | Utiliser EProver externe |
Modules TweetyProject Couverts
Logiques (Notebooks 2-3)
| Module | Description | Notebook |
|---|---|---|
logics.pl |
Logique Propositionnelle | 2 |
logics.fol |
Logique du Premier Ordre | 2 |
logics.dl |
Logique de Description | 3 |
logics.ml |
Logique Modale | 3 |
logics.qbf |
Quantified Boolean Formulas | 3 |
logics.cl |
Logique Conditionnelle | 3 |
logics.mln |
Markov Logic Networks (FOL pondérée) | 10 |
causal |
Raisonnement causal (do-calculus, SCM, contrefactuels) | 11 |
Révision de Croyances (Notebook 4)
| Module | Description |
|---|---|
beliefdynamics |
Opérateurs de révision AGM |
logics.pl.analysis |
Mesures d’incohérence |
logics.pl.sat |
MUS, MaxSAT |
Argumentation (Notebooks 5-7)
| Module | Description | Notebook |
|---|---|---|
arg.dung |
Frameworks de Dung | 5 |
arg.aspic |
ASPIC+ | 6 |
arg.delp |
Defeasible Logic Programming | 6 |
arg.aba |
Assumption-Based Argumentation | 6 |
lp.asp |
Answer Set Programming | 6 |
arg.adf |
Abstract Dialectical Frameworks | 7a |
arg.bipolar |
Frameworks Bipolaires | 7a |
arg.weighted |
Frameworks Pondérés | 7a |
arg.social |
Argumentation Sociale | 7a |
arg.setaf |
Attaques Collectives | 7a |
arg.extended |
Attaques Récursives | 7a |
arg.rankings |
Sémantiques de Classement | 7b |
arg.prob |
Argumentation Probabiliste | 7b |
Agents et Préférences (Notebooks 8-9)
| Module | Description | Notebook |
|---|---|---|
agents |
Framework agents de base | 8 |
agents.dialogues |
Dialogues argumentatifs | 8 |
agents.dialogues.oppmodels |
Jeux grounded (ArguingAgent) | 8 |
agents.dialogues.lotteries |
Loteries argumentatives | 8 |
preferences |
Ordres de préférence, agrégation | 9 |
Validation des Notebooks
Script de vérification
cd MyIA.AI.Notebooks/SymbolicAI/Tweety/scripts
# Vérification structurelle rapide
python verify_all_tweety.py --quick
# Vérification environnement
python verify_all_tweety.py --check-env
# Analyse des sorties existantes
python verify_all_tweety.py --analyze-outputs --verbose
# Exécution complète (lent)
python verify_all_tweety.py --execute --verbose
# Notebook spécifique
python verify_all_tweety.py --notebook Tweety-2 --analyze-outputsOptions disponibles
| Option | Description |
|---|---|
--quick |
Validation structure uniquement |
--check-env |
Vérifier JDK, JARs, outils |
--analyze-outputs |
Analyser sorties existantes |
--execute |
Exécution Papermill complète |
--cell-by-cell |
Exécution cellule par cellule |
--execute-missing |
Exécuter cellules sans output |
--clean-errors |
Nettoyer sorties en erreur |
--verbose |
Sortie détaillée |
--json |
Format JSON (CI/CD) |
FAQ / Troubleshooting
JPypeError ou JVM déjà démarrée
Tweety utilise JPype pour intégrer la JVM. Si un notebook signale que la JVM est déjà démarrée, c’est que le notebook précédent ne l’a pas arrêtée proprement. Relancer Jupyter et exécuter depuis le notebook 1.
Clingo non trouvé
Si clingo n’est pas dans le PATH, utiliser le script de téléchargement :
python scripts/download_tweety_tools.py --clingoLe binaire Windows sera téléchargé dans ext_tools/.
EProver ne répond pas ou heap space
EProver peut bloquer sur des formules FOL complexes avec égalité. La solution est d’utiliser un solveur plus léger ou de réduire la taille de la base de connaissances. Voir la section “Limitations connues” ci-dessus.
Erreur de chargement d’un JAR Tweety
Vérifier que la version Tweety dans Tweety-01-Setup-Python.ipynb correspond à la version téléchargée. La version recommandée est 1.30. Pour changer de version, modifier la variable TWEETY_VERSION puis relancer le notebook 1.
ClassCastException en argumentation
Le notebook 5 signale un bug connu (AF Learning — ClassCastException). La section correspondante est désactivée. Suivre les autres sections sans problème.
JPype lent au premier appel
Le premier appel à un module Java déclenche le chargement de la JVM et des classes Tweety. Attendez 5-10 secondes avant la première réponse. Les appels suivants sont rapides.
Comment passer d’un notebook à l’autre ?
Chaque notebook présuppose la configuration faite dans Tweety-1-Setup (JDK, JARs, JVM). Une fois le notebook 1 exécuté, les notebooks 2-9 peuvent être exécutés dans l’ordre logique de la série. Les outils externes (Clingo, SPASS, EProver) sont configurés par le notebook 1.
Versions TweetyProject
| Version | Date | Nouveautés |
|---|---|---|
| 1.28 | Janvier 2025 | arg.caf, k-admissibility, API refactoring |
| 1.29 | Juillet 2025 | arg.eaf (Epistemic AF), graph rendering |
| 1.30 | Janvier 2026 | causal reasoning, arg.explanations, equivalence checking |
La version est configurable dans Tweety-01-Setup-Python.ipynb (variable TWEETY_VERSION). La version 1.30 est recommandée — elle inclut les sémantiques de causalité, les explications en argumentation, et le checking d’équivalence de frameworks.
Ressources
Références académiques
| Référence | Couverture |
|---|---|
| Dung, “On the Acceptability of Arguments” (1995) | Notebook 5, sémantiques de Dung |
| Modgil & Prakken, “The ASPIC+ Framework” (2014) | Notebook 6, argumentation structurée |
| Alchourron, Gardenfors & Makinson, “On the Logic of Theory Change” (1985) | Notebook 4, révision AGM |
| Enderton, A Mathematical Introduction to Logic (2001) | Notebooks 2-3, logiques formelles |
| Besnard & Hunter, Elements of Argumentation (2008) | Notebooks 5-7, théorie argumentation |
| Brewka, Eiter & Truszczynski, “Answer Set Programming at a Glance” (2011) | Notebook 6, ASP/Clingo |
| Russell & Norvig, AIMA 4e éd., ch. 7-8 | Cadre général logique et SAT |
| Gärdenfors & Makinson (1988) | Notebook 4, enracinement épistémique (caractérisation AGM) |
| Caminada (2006); Modgil & Caminada (2009) | Notebook 5, labellings trivalués (in/out/undec) |
| Baroni et al. (2005) | Notebook 5, sémantique CF2 (cycles impairs) |
| García & Simari, “Defeasible Logic Programming” (2004) | Notebook 6, DeLP |
| Brewka & Woltran, “Abstract Dialectical Frameworks” (2010) | Notebook 7a, ADF |
| Cayrol & Lagasquie-Schiex (2005) | Notebook 7a, frameworks bipolaires (BAF) |
| Bonzon, Delobelle, Konieczny & Maudet (2016) | Notebook 7b, sémantiques de classement |
| Arrow, “Social Choice and Individual Values” (1951) | Notebook 9, théorème d’impossibilité (choix social) |
Ressources en ligne
- TweetyProject : https://tweetyproject.org/
- Documentation API : https://tweetyproject.org/api/
- GitHub : https://github.com/TweetyProjectTeam/TweetyProject
- JPype : https://jpype.readthedocs.io/
Ponts avec les autres séries
| Série | Connection | Détails |
|---|---|---|
| Argument_Analysis | Argumentation agentique | Utilise Tweety comme backend Java pour le raisonnement argumentatif. Les sémantiques de Dung (notebook 5) sont directement appliquées dans l’analyse de textes. |
| Lean | Vérification formelle | Les logiques propositionnelles et FOL (notebooks 2-3) correspondent aux tactiques de preuve Lean. Les SAT solvers de Tweety complètent la vérification Lean. |
| SmartContracts | Méthodes formelles | La vérification formelle SC-14 (Certora/SMTChecker) utilise les mêmes solveurs SAT/SMT. La logique propositionnelle de Tweety est la base des invariants Solidity. |
| SemanticWeb | Logique de Description / OWL | La logique de Description (Tweety-3) est le fondement du raisonnement OWL : les ontologies OWL DL (SW-6/SW-7) utilisent les mêmes solveurs DL que Tweety. |
| GameTheory | Théorie du vote | Le notebook 9 (Préférences/Vote) couvre les concepts de choix social formalisés dans game_theory_lean/SocialChoice/ (Arrow, Sen, Voting). |
| Planners | Planification argumentative | Les dialogues argumentatifs (notebook 8) peuvent être modélisés comme des problèmes de planification PDDL. |
| Lecture transversale | La mer qui monte | Grille de lecture grothendieckienne du dépôt : changement de représentation, certification A/B/C |
Conclusion / Prochaines étapes
Ce que vous avez appris
Tweety est l’outil où le raisonnement devient explicite et vérifiable — le contre-pied des approches purement statistiques. En parcourant cette série, vous êtes allé du connecteur booléen au débat multi-agent :
- Les logiques classiques (notebooks 1-4) : propositionnelle, du premier ordre, modale, de description. Vous avez vu qu’un même énoncé se décide mécaniquement — un SAT solver tranche, un reasoner DL classe, sans intuition.
- L’argumentation (notebooks 5-7b) : la contribution la plus originale de Tweety. Les frameworks de Dung, ASPIC+, ABA, ADF, l’argumentation bipolaire et probabiliste — chaque modèle définit non pas « quelle conclusion est vraie » mais « quel argument résiste à l’attaque ». C’est une logique du débat, pas de la vérité.
- Les applications (notebooks 8-9) : dialogues multi-agents, révision de croyances AGM, préférences et vote. La boucle se ferme — du raisonnement individuel à la délibération collective.
Prochaines étapes
- Appliquez l’argumentation à du texte réel : la série Argument_Analysis utilise Tweety comme backend pour analyser des argumentations naturelles — c’est le terrain où les sémantiques de Dung rencontrent du langage humain.
- Certifiez : les SAT/SMT solvers de Tweety et la vérification formelle partagent le même socle. La série Lean pousse la logique jusqu’à la preuve de programmes ; SmartContracts (SC-14) l’applique aux invariants Solidity.
- Reliez aux ontologies : la logique de description de Tweety-3 est le moteur de raisonnement OWL. La série SemanticWeb (SW-6/SW-7) en fait le cœur des graphes de connaissances.
- Élargissez au choix social : le notebook 9 (vote, préférences) est la porte d’entrée vers la théorie du choix social formalisée en Lean dans la série GameTheory (Arrow, Sen, Voting).
- Les six ponts détaillés ci-dessus (
## Ponts avec les autres séries) cartographient l’ensemble de ces connexions ; la Lecture transversale les relie au fil rouge du dépôt.
Le fil rouge
Le pitch de Tweety tient en un mot : explicabilité. Là où un LLM produit une réponse, Tweety produit un argument — une chaîne de raisonnement inspectable, attaquable, défendable. Les logiques changent (propositionnelle, FOL, modale, DL), les frameworks changent (Dung, ASPIC+, ABA), mais l’exigence reste — raisonner de façon transparente, pas opaquement. C’est elle que vous emportez au-delà de cette série, et c’est ce qui fait de l’IA symbolique un garde-fou naturel pour l’IA générative.
Version 1.2.6 — Septembre 2026 — entrée README de Tweety-02f-Modal-Zoo-Lean-Python (tranche G de l’EPIC #15066, sous-cube modal certifié : le module FormalLogic.ModalZoo (#17642) porte huit systèmes normaux et l’ordre** qui les relie ; le notebook exporte ses trois listes par lake env lean (toJson, récupéré entre marqueurs — aucune recopie), recalcule l’ordre en Python à partir des seuls profils exportés (le droit de le faire étant le théorème weakerThan_iff_profile), puis dessine le diagramme de Hasse — 11 arêtes de couverture et 7 paires incomparables, sur les 28 paires du cube, 21 inclusions strictes dont 10 par transitivité ; trois exercices stubs C.1). Surfaces touchées : table Structure (+ entrée 2f), table « En quoi chaque notebook est unique » (+ entrée), arbre de structure, tableau des stacks (colonne Python) et statistiques par sous-catégorie (Lean companion 6 → 7, total 38 → 39). Écart mesuré et corrigé au passage : la vue d’ensemble annonçait 1165 cellules pour 37 racine + 1 probe ; le disque en portait 1150 (1138 racine + 12 probe) — l’addition du notebook porte le compte à 1170 (446 code). Les 438 cellules de code, elles, étaient exactes. Résidus déclarés, non comblés ici : Tweety-12-Grounded-Via-TweetyProject reste absent des deux tables (13e notebook Python, durée jamais déclarée — même résidu que v1.2.3 à v1.2.5, aucune ligne inventée) ; la ligne « Durée estimée ~6h (tutorat) » n’est pas re-dérivée (notion distincte de la somme par notebook) ; et le bloc CATALOG-STATUS (pedagogical_count: 36) n’est pas réécrit à la main — il décrit main avant l’ajout et se résorbera à la prochaine régénération (catalog-pr-hygiene). Précédent : Version 1.2.5 — Septembre 2026 — entrée README de Tweety-02e-Preuves-Hilbert-Gentzen-Lean (tranche D de l’EPIC #15066, atelier calculs de preuve : les trois axiomes de Hilbert vérifiés par deux oracles réels, une preuve construite par chaînage avant — coût mesuré en instances/MP, plus une contre-expérience qui réfute par la mesure l’hypothèse d’un vivier simplement trop étroit — le syllogisme hypothétique, valide pour les deux oracles, n’est pas dérivé par le moteur, et l’élargir aux sous-formules de la cible ne suffit pas — puis le calcul des séquents LK dont la hauteur et la taille sont mesurées avant/après élimination des coupures, le Hauptsatz étant invoqué comme théorème du noyau Derivation.Canonical.constructiveHauptsatz, témoin IsCutFree inclus). Surfaces touchées : table Structure (+ entrée 2e), table « En quoi chaque notebook est unique » (+ entrée), arbre de structure, statistiques par sous-catégorie (Lean companion 4 → 6, total 35 → 38 — le recensement inclut désormais Tweety-12-Grounded-Via-TweetyProject, jusqu’ici hors comptes, avec sa maturité déclarée absente plutôt qu’inventée) et colonne Python du tableau des stacks (16 → 18). Le même geste comble un écart non déclaré : Tweety-02d-FOL-Lab-Lean (tranche B, #16877), présent sur disque depuis sa livraison mais absent des deux tables, y entre avec sa propre durée déclarée (45 minutes, lue dans le notebook) — aucune durée inventée. Trois écarts mesurés et corrigés au passage : les comptes de notebooks (« 32 » de la vue d’ensemble → 37 racine, dont 36 tabulés ; 34 → 36 principaux), les cellules totales (916 → 1165, mesurées sur l’ensemble des fichiers de la série) et les durées agrégées (Python ~13h, C#/.NET ~10h — la somme de la colonne C# valait déjà 585 min contre « ~7h » annoncées) ; l’arbre annonçait par ailleurs 18 assemblages .NET, git ls-tree origin/main en compte 19. Résidus déclarés, non comblés ici : Tweety-12-Grounded-Via-TweetyProject reste absent des tables (13e notebook Python ; sa durée n’est déclarée nulle part — même résidu que v1.2.3 et v1.2.4, aucune ligne inventée) ; la ligne « Durée estimée ~6h (tutorat) » de la vue d’ensemble n’est pas re-dérivée (notion distincte de la somme par notebook, non mesurable depuis le disque) ; et le versant Lean de la tranche D reste dans le notebook — les deux fichiers d’index du lake (FormalLogic/../FormalLogic.lean et son README.md) sont sous claim actif d’une autre lane (check_lane_claim.py, verdict BLOCKED au 2026-09-25), aucun module de pont n’a donc été ajouté à formal_logic_lean/. Précédent : Version 1.2.4 — Septembre 2026 — entree README de Tweety-3b-Modal-Lab-Lean (tranche C de l’EPIC #15066, laboratoire modal croise Python/Kripke <-> Lean/ModalBridge #17017) : table Structure (+ entrée 3b, notebooks principaux 33 → 34), table « En quoi chaque notebook est unique » (+ entrée), arbre de structure, statistiques par sous-categorie (Lean companion 3 → 4, total 34 → 35) et colonne Python du tableau des stacks (15 → 16). Residu declare, non comble ici : Tweety-12-Grounded-Via-TweetyProject reste absent des tables (duree non declaree, cf. v1.2.3). Precedent : Version 1.2.3 — Septembre 2026 — entree README de Tweety-5e-Propositional-Lab-Lean (tranche A de l’EPIC #15066, laboratoire propositionnel Tweety/Lean) : table Structure (notebooks principaux 32 → 33), table « En quoi chaque notebook est unique » (ajout de 5d et 5e, lignes 31 → 33), arbre de structure, statistiques par sous-categorie (Lean companion 2 → 3, total 33 → 34) et colonne Python du tableau des stacks (14 → 15). Residu declare, non comble ici : Tweety-12-Grounded-Via-TweetyProject (13e notebook Python, kernel python3, execute 8/8 sans erreur) reste absent des tables — sa duree n’est declaree nulle part dans le notebook, aucune ligne n’a donc ete inventee. Precedent : Version 1.2.2 — Août 2026 — ajout Tweety-5d (synthèse certifiée Z3→Lean, Loi II #12205/#13597) : lake argumentation_lean 6+6 siblings _en (module Synthesis), toolchain corrigée v4.32.1 (#11587), comptes re-mesurés : notebooks 33, cellules 969 dont 390 code (périmètre : 32 Tweety-* + 1 probe). Précédent : Version 1.2.1 — re-audit fichier-entier §E : 18 DLLs shades, scripts/ 5+4+_archive, pin IKVM 8.14, limitations re-ancrées 1.30. EPIC #3975 tranche tweety.**
Statistiques catalogue à jour
Statistiques détaillées de la sous-série Tweety. Le pedagogical_count: 36 est lu depuis le marqueur <!-- CATALOG-STATUS --> (l. 5-10). Le détail par sous-catégorie ci-dessous est réconcilié avec les étiquettes par-notebook du tableau Structure (source granulaire). NB : le marqueur indique maturity: BETA=33, ALPHA=3 — l’heuristique catalogue ne distingue pas les statuts PROD/BETA/DRAFT du tableau Structure (qui fait foi au niveau granulaire, DRAFT = Tweety-3-Advanced-Logics-Csharp BROKEN inclus) ; la prose ne s’aligne donc pas sur le marqueur (cf. catalog-pr-hygiene : ne pas s’aligner sur un catalogue faux). Un écart d’une unité subsiste, et il est attendu : le marqueur, régénéré par l’automatisation, décrit main avant l’ajout de Tweety-02e (36 racine), quand le recensement de cette page en compte 38 — le bloc CATALOG-STATUS n’est jamais réécrit à la main sur une branche feature (catalog-pr-hygiene), la résorption se fait donc à la prochaine régénération, pas ici :
| Sous-catégorie | NB | Statut |
|---|---|---|
| Python (Tw-1..11) | 12 | PROD=12 |
Tweety-12-Grounded (non tabulé) |
1 | maturité non déclarée |
| Lean companion (2d, 2e, 2f, 3b, 5b, 5d, 5e) | 7 | BETA=7 |
| C#/.NET | 18 | PROD=12, BETA=5, DRAFT=1 |
Probe _probes/ |
1 | BETA |
| Total | 39 | PROD=24, BETA=13, DRAFT=1, non déclarée=1 |
Détails paradigmes/stacks :
- Python (JPype, 13 nb) : PL/FOL/DL/ML/QBF/CL/Dung/ASPIC+/AGM/MLN/do-calculus Pearl — double stack sur Tw-3 (DL+Modale+QBF), Tw-4 (Belief Revision), Tw-7b (Ranking), Tw-9 (vote/préférences), Tw-10 (MLN), Tw-11 (causal). Tous PROD. Les sept companions Lean viennent en supplément :
Tweety-02d-FOL-Lab-Lean(BETA, kernels Python + Lean, tranche B de l’EPIC #15066 : un même syllogisme exécuté parSimpleFolReasoneret certifié sur le corpus FFL épinglé — conséquences quantifiées, contre-modèles finis exhibés) etTweety-02e-Preuves-Hilbert-Gentzen-Lean(BETA, kernels Python + Lean, tranche D de l’EPIC #15066 : axiomes de Hilbert vérifiés par deux oracles, preuve construite par chaînage avant, puis hauteur/taille d’une dérivation LK avant/après élimination des coupures par le Hauptsatz du noyau), puisTweety-5b-Lean-Argumentation(BETA, kernel Lean 4,argumentation_lean/) etTweety-5d-Stable-Synthesis-Lean(BETA, kernel Python + Z3, Loi II #12205 : spécification → générateur Z3 → témoin → certificat Leanby decide), ainsi queTweety-5e-Propositional-Lab-Lean(BETA, kernels Python + Lean, tranche A de l’EPIC #15066 : trois formules-témoins lues par Tweety, recomptées en Python et certifiées sur Foundation (FFL) au commit épinglé) etTweety-3b-Modal-Lab-Lean(BETA, kernel Python + Lean via WSL, tranche C de l’EPIC #15066 : schémasK/T/4/5parsés parMlParser, énumérés sur les 512 cadres Kripke 3-mondes puis certifiés par le pontFormalLogic.ModalBridge#17017 — réponse sémantique au bug SPASS #1334), etTweety-02f-Modal-Zoo-Lean-Python(BETA, kernels Python + Lean, tranche G de l’EPIC #15066 : le sous-cubeFormalLogic.ModalZoo— profils, couvertures et paires incomparables exportés parlake env lean, ordre recalculé en Python, diagramme de Hasse dessiné et chaque trait certifié par le noyau). - C#/.NET (IKVM 8.14, 18 nb) : bytecode Java→.NET downgrade Java 15→8 (post-C190
JvmDowngrader), sans JVM. PROD=12, BETA=5 (Tweety-2b-Semantics-Csharp,Tweety-2c-FOL-Csharp,Tweety-4-Belief-Revision-Csharp,Tweety-4-Aspic-Csharp,Tweety-5-Abstract-Argumentation-Csharp), DRAFT=1 = BROKEN (Tweety-3-Advanced-Logics-Csharp, conflits de noms surlogics.ml+logics.cl+logics.qbfsimultanés dans la même DLL). - Probe (
_probes/Tweety-IKVM-Init-Probe, 1 nb) : IKVM init smoke-test BETA.
Conformité C.1 : les notebooks exposent des stubs conformes (pass / return None / print("Exercice à compléter") / jamais raise NotImplementedError) et restent exécutables end-to-end. Les dépendances sont gérées par requirements.txt racine (JPype1, tweety-translate, pandas, numpy, jdk-pywrap). Le port C#/.NET (EPIC #4667) cible .NET 9.0 + IKVM 8.14 (post-C190 JvmDowngrader Java 15→8) ; voir la chaîne de build dans .github/workflows/tweety-csharp.yml et l’inventaire détaillé dans la Section Tweety. Le seul notebook C# à maturité DRAFT est Tweety-3-Advanced-Logics-Csharp (statut BROKEN : héritage des conflits de noms de classes IKVM 8.14 sur logics.ml + logics.cl + logics.qbf simultanés).
Écosystème MCP et parenté cross-lane
Trois outils d’infrastructure MCP soutiennent l’exécution, la validation et la composition cross-séries de cette sous-série :
- MCP Jupyter (
mcp__jupyter-papermill__*) — exécution programmée des notebooks via Papermill, capture des sorties, gestion du cycle de vie des kernels Python 3 et.net-csharp. Note : le mode async ignorekernel_name(bug #5211) — toujours passer parnbconvert --executeavec timeout pour les ré-exécutions. - Validation pre-commit (
.pre-commit-config.yaml) — gitleaks (anti-secrets inline, règleos.getenv("KEY", "<literal-fallback>")proscrit) + notebook validator (C.1/C.2 : pas deraise NotImplementedError, cellules code =execution_count+outputscohérents) bloquent les PRs qui dégraderaient les contrats inter-séries. - MCP QC Cloud (
mcp__qc-mcp-lite__*) — backtest QuantConnect partagé pour les notebooks QC (Tw-9 vote Preferences éclaire les modèles de choix social, cf. cross-lane ci-dessous).
La sous-série Tweety s’inscrit dans un réseau cross-lane structuré autour de l’argumentation et de la logique formelle :
| Cette sous-série | Symétrie dans | Pont pédagogique |
|---|---|---|
| Tweety-3 (logique de description) | SemanticWeb (SW-6/SW-7 OWL) | DL = moteur de raisonnement OWL ; même formalisme, deux écosystèmes |
| Tweety-3 (Dung frameworks) | Argument_Analysis | Détection de sophismes via cadres de Dung + Semantic Kernel (LLM-contrôle) |
| Tweety-3 (logique modale/QBF) | Lean (mathlib4) | Formalisation des logiques Tweety dans l’assistant de preuve Lean 4 |
| Tweety-9 (préférences, vote) | GameTheory | Préférences individuelles → fonction de choix social (Borda, Condorcet, Arrow) |
| Tweety-4 (révision AGM) | SmartContracts (SC-14) | Mise à jour de croyances → invariants Solidity, logique de révision on-chain |
| Tweety-11 (Causalité, do-calculus) | ML (inférence causale) | do-calculus Pearl ↔︎ modèles causaux structurels (Pearl 2009) |
Effet de composition : Tweety est le carrefour logique du dépôt — chaque sous-série partenaire (Lean, SemanticWeb, Argument_Analysis, GameTheory, SmartContracts, ML) y trouve un point d’entrée formel vers l’argumentation computationnelle. Le pipeline complet relie les notebooks (qui motivent la pertinence du raisonnement explicite) aux ports C#/.NET (qui rendent Tweety invocable sans JVM, via IKVM 8.14, EPIC #4667) et aux lakes (qui formalisent les théorèmes sous-jacents, ex. Arrow en Lean 4).
Licence
Les notebooks sont distribués sous licence MIT. TweetyProject est sous licence LGPL 3.0.
Comment lire ce README
Le dépôt se lit à trois vitesses (choisir sa vitesse de lecture) ; la série Tweety aussi :
*-Lean*Ce README ne liste plus les notebooks un par un dans une table plate : la table Structure ci-dessous distingue le parcours principal (numéros nus, lisibles de haut en bas) des approfondissements (lettres) et des sous-séries (Argumentation). Le compte exact des notebooks et leur maturité vivent dans le bloc
CATALOG-STATUSci-dessus, régénéré chaque jour par la CI — il fait foi au niveau granulaire.Lire un nom de fichier
Un nom de notebook Tweety suit la forme
Tweety-<NN>[<lettre>]-<Titre>-<Noyau?>.ipynb:01–12Tweety-01-Setup-PythonTweety-02b-Semantics-CSharp02, facultatif-Python/-CSharp/-Lean/-Lean-PythonTweety-3b-Modal-Lab-Lean-Lean-Pythondésigne un notebook Python qui pilote Lean-CSharpvs-CsharpTweety-10-MLN-CsharpvsTweety-02-Basic-Logics-CSharpLa normalisation des noms est en cours (#16231) — la colonne Stack des tables fait foi.