From df657b804b8e4babcfb70bca9f7541453b298e45 Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Thu, 8 Oct 2026 07:24:36 +0200 Subject: [PATCH 1/2] Fix(#18064): Tweety README -- 22 liens .html casses -> .ipynb + requalification Tweety-12 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Le rename #16231 PR-b (a3c5742cd6, #19502) a introduit des suffixes .html sur les rangees renommees : 22 cibles *.html referencees, aucune n'existe sur disque (0 fichier .html dans le dossier), chacune a un sibling .ipynb existant. Remplacement de suffixe sur les 22 liens. Requalification factuelle de la ligne de statistiques : Tweety-12-Grounded etait qualifie « non tabule » alors que la table racine le tabule en rangee 12. Le changelog v1.2.6 (l.828) n'est pas touche : entree historique datee. Aucun total ni compte regenere a la main (#17029, catalog-pr-hygiene). Post-fix : 65 liens internes, 0 manquant, 0 .html restant. Co-Authored-By: Claude Haiku 4.5 (1M context) --- MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md b/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md index 87edcbe954..7a11ddc3c5 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md @@ -174,16 +174,16 @@ Numéros nus uniquement, lisibles de haut en bas. Le compte et la maturité exac |---|----------|--------------------|-------| | 1 | [Tweety-01-Setup-Python](Tweety-01-Setup-Python.ipynb) | Configuration JVM, JARs, solveurs externes | Python | | 2 | [Tweety-02-Basic-Logics-Python](Tweety-02-Basic-Logics-Python.ipynb) | Logique propositionnelle (SAT) et du premier ordre (FOL) | Python | -| 3 | [Tweety-03-Advanced-Logics-Python](Tweety-03-Advanced-Logics-Python.html) | DL, Modale, QBF, Conditionnelle | Python | -| 4 | [Tweety-04-Belief-Revision-Python](Tweety-04-Belief-Revision-Python.html) | MUS, MaxSAT, Mesures d'incohérence, AGM | Python | -| 5 | [Tweety-05-Abstract-Argumentation-Python](Tweety-05-Abstract-Argumentation-Python.html) | Dung AF, sémantiques grounded/stable/CF2 | Python | +| 3 | [Tweety-03-Advanced-Logics-Python](Tweety-03-Advanced-Logics-Python.ipynb) | DL, Modale, QBF, Conditionnelle | Python | +| 4 | [Tweety-04-Belief-Revision-Python](Tweety-04-Belief-Revision-Python.ipynb) | MUS, MaxSAT, Mesures d'incohérence, AGM | Python | +| 5 | [Tweety-05-Abstract-Argumentation-Python](Tweety-05-Abstract-Argumentation-Python.ipynb) | Dung AF, sémantiques grounded/stable/CF2 | Python | | 6 | [Tweety-06-Structured-Argumentation-Python](Tweety-06-Structured-Argumentation-Python.ipynb) | ASPIC+, DeLP, ABA, ASP | Python | | 7 | [Tweety-07a-Extended-Frameworks-Python](Tweety-07a-Extended-Frameworks-Python.ipynb) | ADF, Bipolar, WAF, SAF, SetAF, Extended | Python | | 8 | [Tweety-08-Agent-Dialogues-Python](Tweety-08-Agent-Dialogues-Python.ipynb) | Agents, dialogues argumentatifs, loteries | Python | | 9 | [Tweety-09-Preferences-Python](Tweety-09-Preferences-Python.ipynb) | Préférences, théorie du vote | Python | -| 10 | [Tweety-10-MLN-Python](Tweety-10-MLN-Python.html) | Markov Logic Networks (FOL pondérée) | Python | -| 11 | [Tweety-11-Causal-Python](Tweety-11-Causal-Python.html) | do-calculus de Pearl, interventions, contrefactuels | Python | -| 12 | [Tweety-12-Grounded-Via-TweetyProject-Python](Tweety-12-Grounded-Via-TweetyProject-Python.html) | Bouclage de la sémantique grounded entre Python et Lean | Python | +| 10 | [Tweety-10-MLN-Python](Tweety-10-MLN-Python.ipynb) | Markov Logic Networks (FOL pondérée) | Python | +| 11 | [Tweety-11-Causal-Python](Tweety-11-Causal-Python.ipynb) | do-calculus de Pearl, interventions, contrefactuels | Python | +| 12 | [Tweety-12-Grounded-Via-TweetyProject-Python](Tweety-12-Grounded-Via-TweetyProject-Python.ipynb) | 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. @@ -198,36 +198,36 @@ Une section par palier qui ouvre des lettres. Chaque lettre est **facultative** | 02a | [Tweety-02-Basic-Logics-CSharp](Tweety-02-Basic-Logics-CSharp.ipynb) | Jumeau C#/.NET du 02 (IKVM, **port pilote** #4792, premier pont Java→.NET de la série) | | 02b | [Tweety-02b-Semantics-CSharp](Tweety-02b-Semantics-CSharp.ipynb) | Sémantique propositionnelle .NET (mondes possibles) | | 02c | [Tweety-02c-FOL-CSharp](Tweety-02c-FOL-CSharp.ipynb) | FOL porté .NET via IKVM 8.15.0 (`tweetyproject.logics.fol.*` réel, DLL `tweety-pl` référençant `IKVM.Runtime` 8.15.0) | -| 02d | [Tweety-02d-FOL-Lab-Lean-Python](Tweety-02d-FOL-Lab-Lean-Python.html) | **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-Python](Tweety-02e-Preuves-Hilbert-Gentzen-Lean-Python.html) | **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`) | +| 02d | [Tweety-02d-FOL-Lab-Lean-Python](Tweety-02d-FOL-Lab-Lean-Python.ipynb) | **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-Python](Tweety-02e-Preuves-Hilbert-Gentzen-Lean-Python.ipynb) | **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](Tweety-02f-Modal-Zoo-Lean-Python.ipynb) | **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](https://github.com/jsboige/CoursIA/pull/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-03b-Modal-Lab-Lean-Python](Tweety-03b-Modal-Lab-Lean-Python.html) | **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-03-Advanced-Logics-CSharp](Tweety-03-Advanced-Logics-CSharp.html) | DL/ML/QBF/CL .NET — **DRAFT** : conflits de noms DLL entre `logics.ml` + `logics.cl` + `logics.qbf` simultanés | -| 03c-CL | [Tweety-03-Conditional-Logics-CSharp](Tweety-03-Conditional-Logics-CSharp.html) | Logique conditionnelle .NET (IKVM) — raisonneur `cl` réel | -| 03c-Dung | [Tweety-03-Dung-CSharp](Tweety-03-Dung-CSharp.html) | Argumentation de Dung .NET (IKVM, c.182 PR #5194) — `NaiveDlReasoner` | -| 03c-ML | [Tweety-03-ModalLogic-CSharp](Tweety-03-ModalLogic-CSharp.html) | Logique modale .NET (IKVM) — `MlReasoner` réel | -| 03c-QBF | [Tweety-03-QBF-CSharp](Tweety-03-QBF-CSharp.html) | QBF .NET (IKVM, c.185 PR #5202) — solveur QBF réel | +| 03b | [Tweety-03b-Modal-Lab-Lean-Python](Tweety-03b-Modal-Lab-Lean-Python.ipynb) | **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-03-Advanced-Logics-CSharp](Tweety-03-Advanced-Logics-CSharp.ipynb) | DL/ML/QBF/CL .NET — **DRAFT** : conflits de noms DLL entre `logics.ml` + `logics.cl` + `logics.qbf` simultanés | +| 03c-CL | [Tweety-03-Conditional-Logics-CSharp](Tweety-03-Conditional-Logics-CSharp.ipynb) | Logique conditionnelle .NET (IKVM) — raisonneur `cl` réel | +| 03c-Dung | [Tweety-03-Dung-CSharp](Tweety-03-Dung-CSharp.ipynb) | Argumentation de Dung .NET (IKVM, c.182 PR #5194) — `NaiveDlReasoner` | +| 03c-ML | [Tweety-03-ModalLogic-CSharp](Tweety-03-ModalLogic-CSharp.ipynb) | Logique modale .NET (IKVM) — `MlReasoner` réel | +| 03c-QBF | [Tweety-03-QBF-CSharp](Tweety-03-QBF-CSharp.ipynb) | 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-04-Belief-Revision-CSharp](Tweety-04-Belief-Revision-CSharp.html) | Belief Revision .NET (IKVM) : `Revision`/`MUSMaxSAT` réels | -| 04c-Aspic | [Tweety-04-Aspic-CSharp](Tweety-04-Aspic-CSharp.html) | ASPIC+ .NET (IKVM) — `AspicArgumentation` réel | +| 04c-BR | [Tweety-04-Belief-Revision-CSharp](Tweety-04-Belief-Revision-CSharp.ipynb) | Belief Revision .NET (IKVM) : `Revision`/`MUSMaxSAT` réels | +| 04c-Aspic | [Tweety-04-Aspic-CSharp](Tweety-04-Aspic-CSharp.ipynb) | ASPIC+ .NET (IKVM) — `AspicArgumentation` réel | #### Autour de 05 — argumentation abstraite et compagnons Lean | Lettre | Notebook | Ce que cette lettre ajoute | |---|---|---| -| 05b | [Tweety-05b-Argumentation-Lean](Tweety-05b-Argumentation-Lean.html) | **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-05-Abstract-Argumentation-CSharp](Tweety-05-Abstract-Argumentation-CSharp.html) | 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-05d-Stable-Synthesis-Lean-Python](Tweety-05d-Stable-Synthesis-Lean-Python.html) | **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-05e-Propositional-Lab-Lean-Python](Tweety-05e-Propositional-Lab-Lean-Python.html) | **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) | +| 05b | [Tweety-05b-Argumentation-Lean](Tweety-05b-Argumentation-Lean.ipynb) | **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-05-Abstract-Argumentation-CSharp](Tweety-05-Abstract-Argumentation-CSharp.ipynb) | 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-05d-Stable-Synthesis-Lean-Python](Tweety-05d-Stable-Synthesis-Lean-Python.ipynb) | **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-05e-Propositional-Lab-Lean-Python](Tweety-05e-Propositional-Lab-Lean-Python.ipynb) | **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# @@ -256,8 +256,8 @@ Le palier 07 est porté par le **07a** (Python) et son jumeau **07ac** (C#) ; le | Lettre | Notebook | Ce que cette lettre ajoute | |---|---|---| -| 10c | [Tweety-10-MLN-CSharp](Tweety-10-MLN-CSharp.html) | MLN porté .NET (IKVM, c.188 PR #5209) — `MarkovLogicNetwork`, vrais appels | -| 11c | [Tweety-11-Causal-CSharp](Tweety-11-Causal-CSharp.html) | Twin C# moteur causal booléen from-scratch .NET : do-operator, contrefactuels par mondes jumeaux | +| 10c | [Tweety-10-MLN-CSharp](Tweety-10-MLN-CSharp.ipynb) | MLN porté .NET (IKVM, c.188 PR #5209) — `MarkovLogicNetwork`, vrais appels | +| 11c | [Tweety-11-Causal-CSharp](Tweety-11-Causal-CSharp.ipynb) | Twin C# moteur causal booléen from-scratch .NET : do-operator, contrefactuels par mondes jumeaux | ### Sous-série Argumentation — Argumentum @@ -834,7 +834,7 @@ Statistiques détaillées de la sous-série Tweety. Le `pedagogical_count: 36` e | Sous-catégorie | NB | Statut | |-----------------------|-------|------------------------------| | Python (Tw-1..11) | 12 | PROD=12 | -| `Tweety-12-Grounded` (non tabulé) | 1 | maturité non déclarée | +| `Tweety-12-Grounded` (rangée 12 de la table racine) | 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 | From 71f0c37c675108bc851eae6c8ad4844561f761ed Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Thu, 8 Oct 2026 07:57:02 +0200 Subject: [PATCH 2/2] Fix(#18064): uniformiser Tweety README sur la convention #13025 (.html rendu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Le commit precedent convertissait 22 liens .html -> .ipynb : sens inverse de la convention. #13025 : un notebook dans la render-list Quarto se lie par son sibling .html (le .ipynb brut 404 sur Pages) ; l'organe readme-ipynb-links-guard classe tout lien .ipynb vers la render-list en STALE_LINK. Les 22 liens sont restaures en .html. Elargissement (E) : les 19 STALE_LINK preexistants du README racine (16 notebooks Tweety + 3 cross-series Probas/IIT lies en .ipynb) sont aussi convertis en .html -- le README racine passe a 0 violation a l'organe (mesure : 19 -> 0). La requalification Tweety-12 « rangee 12 de la table racine » est conservee (finding changelog-vs-table, toujours valide). Co-Authored-By: Claude Haiku 4.5 (1M context) --- MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md | 82 +++++++++---------- 1 file changed, 41 insertions(+), 41 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md b/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md index 7a11ddc3c5..2cc2f6916f 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md @@ -172,18 +172,18 @@ Numéros nus uniquement, lisibles de haut en bas. Le compte et la maturité exac | # | Notebook | Ce qu'on y apprend | Stack | |---|----------|--------------------|-------| -| 1 | [Tweety-01-Setup-Python](Tweety-01-Setup-Python.ipynb) | Configuration JVM, JARs, solveurs externes | Python | -| 2 | [Tweety-02-Basic-Logics-Python](Tweety-02-Basic-Logics-Python.ipynb) | Logique propositionnelle (SAT) et du premier ordre (FOL) | Python | -| 3 | [Tweety-03-Advanced-Logics-Python](Tweety-03-Advanced-Logics-Python.ipynb) | DL, Modale, QBF, Conditionnelle | Python | -| 4 | [Tweety-04-Belief-Revision-Python](Tweety-04-Belief-Revision-Python.ipynb) | MUS, MaxSAT, Mesures d'incohérence, AGM | Python | -| 5 | [Tweety-05-Abstract-Argumentation-Python](Tweety-05-Abstract-Argumentation-Python.ipynb) | Dung AF, sémantiques grounded/stable/CF2 | Python | -| 6 | [Tweety-06-Structured-Argumentation-Python](Tweety-06-Structured-Argumentation-Python.ipynb) | ASPIC+, DeLP, ABA, ASP | Python | -| 7 | [Tweety-07a-Extended-Frameworks-Python](Tweety-07a-Extended-Frameworks-Python.ipynb) | ADF, Bipolar, WAF, SAF, SetAF, Extended | Python | -| 8 | [Tweety-08-Agent-Dialogues-Python](Tweety-08-Agent-Dialogues-Python.ipynb) | Agents, dialogues argumentatifs, loteries | Python | -| 9 | [Tweety-09-Preferences-Python](Tweety-09-Preferences-Python.ipynb) | Préférences, théorie du vote | Python | -| 10 | [Tweety-10-MLN-Python](Tweety-10-MLN-Python.ipynb) | Markov Logic Networks (FOL pondérée) | Python | -| 11 | [Tweety-11-Causal-Python](Tweety-11-Causal-Python.ipynb) | do-calculus de Pearl, interventions, contrefactuels | Python | -| 12 | [Tweety-12-Grounded-Via-TweetyProject-Python](Tweety-12-Grounded-Via-TweetyProject-Python.ipynb) | Bouclage de la sémantique grounded entre Python et Lean | Python | +| 1 | [Tweety-01-Setup-Python](Tweety-01-Setup-Python.html) | Configuration JVM, JARs, solveurs externes | Python | +| 2 | [Tweety-02-Basic-Logics-Python](Tweety-02-Basic-Logics-Python.html) | Logique propositionnelle (SAT) et du premier ordre (FOL) | Python | +| 3 | [Tweety-03-Advanced-Logics-Python](Tweety-03-Advanced-Logics-Python.html) | DL, Modale, QBF, Conditionnelle | Python | +| 4 | [Tweety-04-Belief-Revision-Python](Tweety-04-Belief-Revision-Python.html) | MUS, MaxSAT, Mesures d'incohérence, AGM | Python | +| 5 | [Tweety-05-Abstract-Argumentation-Python](Tweety-05-Abstract-Argumentation-Python.html) | Dung AF, sémantiques grounded/stable/CF2 | Python | +| 6 | [Tweety-06-Structured-Argumentation-Python](Tweety-06-Structured-Argumentation-Python.html) | ASPIC+, DeLP, ABA, ASP | Python | +| 7 | [Tweety-07a-Extended-Frameworks-Python](Tweety-07a-Extended-Frameworks-Python.html) | ADF, Bipolar, WAF, SAF, SetAF, Extended | Python | +| 8 | [Tweety-08-Agent-Dialogues-Python](Tweety-08-Agent-Dialogues-Python.html) | Agents, dialogues argumentatifs, loteries | Python | +| 9 | [Tweety-09-Preferences-Python](Tweety-09-Preferences-Python.html) | Préférences, théorie du vote | Python | +| 10 | [Tweety-10-MLN-Python](Tweety-10-MLN-Python.html) | Markov Logic Networks (FOL pondérée) | Python | +| 11 | [Tweety-11-Causal-Python](Tweety-11-Causal-Python.html) | do-calculus de Pearl, interventions, contrefactuels | Python | +| 12 | [Tweety-12-Grounded-Via-TweetyProject-Python](Tweety-12-Grounded-Via-TweetyProject-Python.html) | 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. @@ -195,45 +195,45 @@ Une section par palier qui ouvre des lettres. Chaque lettre est **facultative** | Lettre | Notebook | Ce que cette lettre ajoute | |---|---|---| -| 02a | [Tweety-02-Basic-Logics-CSharp](Tweety-02-Basic-Logics-CSharp.ipynb) | Jumeau C#/.NET du 02 (IKVM, **port pilote** #4792, premier pont Java→.NET de la série) | -| 02b | [Tweety-02b-Semantics-CSharp](Tweety-02b-Semantics-CSharp.ipynb) | Sémantique propositionnelle .NET (mondes possibles) | -| 02c | [Tweety-02c-FOL-CSharp](Tweety-02c-FOL-CSharp.ipynb) | FOL porté .NET via IKVM 8.15.0 (`tweetyproject.logics.fol.*` réel, DLL `tweety-pl` référençant `IKVM.Runtime` 8.15.0) | -| 02d | [Tweety-02d-FOL-Lab-Lean-Python](Tweety-02d-FOL-Lab-Lean-Python.ipynb) | **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-Python](Tweety-02e-Preuves-Hilbert-Gentzen-Lean-Python.ipynb) | **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](Tweety-02f-Modal-Zoo-Lean-Python.ipynb) | **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](https://github.com/jsboige/CoursIA/pull/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 | +| 02a | [Tweety-02-Basic-Logics-CSharp](Tweety-02-Basic-Logics-CSharp.html) | Jumeau C#/.NET du 02 (IKVM, **port pilote** #4792, premier pont Java→.NET de la série) | +| 02b | [Tweety-02b-Semantics-CSharp](Tweety-02b-Semantics-CSharp.html) | Sémantique propositionnelle .NET (mondes possibles) | +| 02c | [Tweety-02c-FOL-CSharp](Tweety-02c-FOL-CSharp.html) | FOL porté .NET via IKVM 8.15.0 (`tweetyproject.logics.fol.*` réel, DLL `tweety-pl` référençant `IKVM.Runtime` 8.15.0) | +| 02d | [Tweety-02d-FOL-Lab-Lean-Python](Tweety-02d-FOL-Lab-Lean-Python.html) | **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-Python](Tweety-02e-Preuves-Hilbert-Gentzen-Lean-Python.html) | **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](Tweety-02f-Modal-Zoo-Lean-Python.html) | **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](https://github.com/jsboige/CoursIA/pull/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-03b-Modal-Lab-Lean-Python](Tweety-03b-Modal-Lab-Lean-Python.ipynb) | **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-03-Advanced-Logics-CSharp](Tweety-03-Advanced-Logics-CSharp.ipynb) | DL/ML/QBF/CL .NET — **DRAFT** : conflits de noms DLL entre `logics.ml` + `logics.cl` + `logics.qbf` simultanés | -| 03c-CL | [Tweety-03-Conditional-Logics-CSharp](Tweety-03-Conditional-Logics-CSharp.ipynb) | Logique conditionnelle .NET (IKVM) — raisonneur `cl` réel | -| 03c-Dung | [Tweety-03-Dung-CSharp](Tweety-03-Dung-CSharp.ipynb) | Argumentation de Dung .NET (IKVM, c.182 PR #5194) — `NaiveDlReasoner` | -| 03c-ML | [Tweety-03-ModalLogic-CSharp](Tweety-03-ModalLogic-CSharp.ipynb) | Logique modale .NET (IKVM) — `MlReasoner` réel | -| 03c-QBF | [Tweety-03-QBF-CSharp](Tweety-03-QBF-CSharp.ipynb) | QBF .NET (IKVM, c.185 PR #5202) — solveur QBF réel | +| 03b | [Tweety-03b-Modal-Lab-Lean-Python](Tweety-03b-Modal-Lab-Lean-Python.html) | **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-03-Advanced-Logics-CSharp](Tweety-03-Advanced-Logics-CSharp.html) | DL/ML/QBF/CL .NET — **DRAFT** : conflits de noms DLL entre `logics.ml` + `logics.cl` + `logics.qbf` simultanés | +| 03c-CL | [Tweety-03-Conditional-Logics-CSharp](Tweety-03-Conditional-Logics-CSharp.html) | Logique conditionnelle .NET (IKVM) — raisonneur `cl` réel | +| 03c-Dung | [Tweety-03-Dung-CSharp](Tweety-03-Dung-CSharp.html) | Argumentation de Dung .NET (IKVM, c.182 PR #5194) — `NaiveDlReasoner` | +| 03c-ML | [Tweety-03-ModalLogic-CSharp](Tweety-03-ModalLogic-CSharp.html) | Logique modale .NET (IKVM) — `MlReasoner` réel | +| 03c-QBF | [Tweety-03-QBF-CSharp](Tweety-03-QBF-CSharp.html) | 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-04-Belief-Revision-CSharp](Tweety-04-Belief-Revision-CSharp.ipynb) | Belief Revision .NET (IKVM) : `Revision`/`MUSMaxSAT` réels | -| 04c-Aspic | [Tweety-04-Aspic-CSharp](Tweety-04-Aspic-CSharp.ipynb) | ASPIC+ .NET (IKVM) — `AspicArgumentation` réel | +| 04c-BR | [Tweety-04-Belief-Revision-CSharp](Tweety-04-Belief-Revision-CSharp.html) | Belief Revision .NET (IKVM) : `Revision`/`MUSMaxSAT` réels | +| 04c-Aspic | [Tweety-04-Aspic-CSharp](Tweety-04-Aspic-CSharp.html) | ASPIC+ .NET (IKVM) — `AspicArgumentation` réel | #### Autour de 05 — argumentation abstraite et compagnons Lean | Lettre | Notebook | Ce que cette lettre ajoute | |---|---|---| -| 05b | [Tweety-05b-Argumentation-Lean](Tweety-05b-Argumentation-Lean.ipynb) | **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-05-Abstract-Argumentation-CSharp](Tweety-05-Abstract-Argumentation-CSharp.ipynb) | 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-05d-Stable-Synthesis-Lean-Python](Tweety-05d-Stable-Synthesis-Lean-Python.ipynb) | **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-05e-Propositional-Lab-Lean-Python](Tweety-05e-Propositional-Lab-Lean-Python.ipynb) | **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) | +| 05b | [Tweety-05b-Argumentation-Lean](Tweety-05b-Argumentation-Lean.html) | **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-05-Abstract-Argumentation-CSharp](Tweety-05-Abstract-Argumentation-CSharp.html) | 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-05d-Stable-Synthesis-Lean-Python](Tweety-05d-Stable-Synthesis-Lean-Python.html) | **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-05e-Propositional-Lab-Lean-Python](Tweety-05e-Propositional-Lab-Lean-Python.html) | **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](Tweety-06-Structured-Argumentation-CSharp.ipynb) | Twin C# ASPIC+ from-scratch (BCL, pas IKVM ; DeLP/ABA/ASP conceptuel) | +| 06c | [Tweety-06-Structured-Argumentation-CSharp](Tweety-06-Structured-Argumentation-CSharp.html) | Twin C# ASPIC+ from-scratch (BCL, pas IKVM ; DeLP/ABA/ASP conceptuel) | #### Autour de 07 — cadres étendus et probabilistes @@ -241,23 +241,23 @@ Le palier 07 est porté par le **07a** (Python) et son jumeau **07ac** (C#) ; le | Lettre | Notebook | Ce que cette lettre ajoute | |---|---|---| -| 07ac | [Tweety-07a-Extended-Frameworks-CSharp](Tweety-07a-Extended-Frameworks-CSharp.ipynb) | 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](Tweety-07b-Ranking-Probabilistic-Python.ipynb) | Sémantiques de classement (ranking) et argumentation probabiliste | -| 07bc | [Tweety-07b-Ranking-Probabilistic-CSharp](Tweety-07b-Ranking-Probabilistic-CSharp.ipynb) | Jumeau C# du 07b (IKVM, c.179 PR #5231) — `Ranking`, `SubgraphProbability` réels | +| 07ac | [Tweety-07a-Extended-Frameworks-CSharp](Tweety-07a-Extended-Frameworks-CSharp.html) | 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](Tweety-07b-Ranking-Probabilistic-Python.html) | Sémantiques de classement (ranking) et argumentation probabiliste | +| 07bc | [Tweety-07b-Ranking-Probabilistic-CSharp](Tweety-07b-Ranking-Probabilistic-CSharp.html) | 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](Tweety-08-Agent-Dialogues-CSharp.ipynb) | 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](Tweety-09-Preferences-CSharp.ipynb) | Préférences .NET (IKVM, c.180 PR #5268) | +| 08c | [Tweety-08-Agent-Dialogues-CSharp](Tweety-08-Agent-Dialogues-CSharp.html) | 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](Tweety-09-Preferences-CSharp.html) | 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](Tweety-10-MLN-CSharp.ipynb) | MLN porté .NET (IKVM, c.188 PR #5209) — `MarkovLogicNetwork`, vrais appels | -| 11c | [Tweety-11-Causal-CSharp](Tweety-11-Causal-CSharp.ipynb) | Twin C# moteur causal booléen from-scratch .NET : do-operator, contrefactuels par mondes jumeaux | +| 10c | [Tweety-10-MLN-CSharp](Tweety-10-MLN-CSharp.html) | MLN porté .NET (IKVM, c.188 PR #5209) — `MarkovLogicNetwork`, vrais appels | +| 11c | [Tweety-11-Causal-CSharp](Tweety-11-Causal-CSharp.html) | Twin C# moteur causal booléen from-scratch .NET : do-operator, contrefactuels par mondes jumeaux | ### Sous-série Argumentation — Argumentum @@ -343,9 +343,9 @@ La signature du do-calculus — **P(rain | drops) ≠ P(rain | do(drops))** — 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](../../Probas/Infer/Infer-5-Causal-Inference.ipynb) — 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](../../Probas/PyMC/PyMC-05-Causal-Inference.ipynb) — la version **MCMC** avec l'opérateur natif `pm.do` et le contrefactuel par abduction. -- [ICT-05-CausalEmergence-Python](../../IIT/ICT-Series/ICT-05-CausalEmergence-Python.ipynb) — le même `do` monte d'un cran : à **quelle échelle** un système fait-il le plus de travail causal ? +- [Infer-5-Causal-Inference](../../Probas/Infer/Infer-5-Causal-Inference.html) — 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](../../Probas/PyMC/PyMC-05-Causal-Inference.html) — la version **MCMC** avec l'opérateur natif `pm.do` et le contrefactuel par abduction. +- [ICT-05-CausalEmergence-Python](../../IIT/ICT-Series/ICT-05-CausalEmergence-Python.html) — le même `do` monte d'un cran : à **quelle échelle** un système fait-il le plus de travail causal ? Vue d'ensemble des quatre paradigmes : le [README IIT](../../IIT/README.md), section « Ponts causaux : le do-calculus de Pearl à travers les paradigmes ».