Skip to content

Add: densite Tweety C# — interpretations pedagogiques, 3 notebooks sous plancher (See #13410) #16319

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jsboige merged 2 commits into from
Sep 15, 2026
Merged

Add: densite Tweety C# — interpretations pedagogiques, 3 notebooks sous plancher (See #13410) #16319

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
265898b
Add: densite Tweety C# — interpretations pedagogiques, 3 notebooks so…
jsboige Sep 15, 2026
f572ed3
fix(twin-parity,#8057): rebaseline paires Tweety-11 Causal + Tweety-8…
jsboige Sep 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
121 changes: 121 additions & 0 deletions MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-02b-Semantics-CSharp.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,6 +183,20 @@
"Console.WriteLine($\"Tweety (IKVM) reference chargee : {an.Name} v{an.Version} ({new FileInfo(tweetyDll).Length / 1024 / 1024:F1} Mo).\");"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Pourquoi un pont Java→.NET ?** Les cellules de configuration ci-dessus chargent la bibliothèque\n",
"**TweetyProject** — écrite en Java — *dans* le processus .NET, via IKVM (une réimplémentation du\n",
"runtime Java en bytecode .NET). Le choix pédagogique est assumé : TweetyProject est l'implémentation\n",
"de référence des logiques pour agents (argumentation, croyances, préférences), maintenue et testée\n",
"par la communauté ; la réécrire « pour faire C# » perdrait ce référentiel. Le pont rend les deux\n",
"mondes comparables : même signature, mêmes mondes, mêmes verdicts — et le jour où un twin C#\n",
"from-scratch existe pour un module, la parité se **mesure** contre cette référence au lieu d'être\n",
"supposée."
]
},
{
"cell_type": "markdown",
"id": "m22726",
Expand Down Expand Up @@ -290,6 +304,20 @@
"Console.WriteLine($\"=> {n} mondes pour 2 atomes (2^2 = 4).\");\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**La structure des mondes.** Les quatre mondes affichés ne sont pas une liste plate : ordonnés par\n",
"inclusion (`[]` ⊂ `[a]` ⊂ `[a,b]`), ils forment le **cube** B_n — l'hypercube des valuations (pour\n",
"2 atomes, un carré ; pour n, un n-cube). Deux propriétés de cette structure servent toute la suite :\n",
"\n",
"- le monde vide `[]` et le monde plein `[a,b]` sont les deux extrêmes (tout-faux / tout-vrai) ;\n",
"- les formules **monotones** (sans négation d'atome) décrivent des *up-sets* du cube — leur ensemble\n",
" de modèles est stable par ajout d'atomes. Les requêtes des sections 3-4 se lisent alors\n",
" géométriquement : intersecter des up-sets, chercher des contre-exemples en descendant."
]
},
{
"cell_type": "markdown",
"id": "m33502",
Expand Down Expand Up @@ -404,6 +432,23 @@
"Console.WriteLine($\" w satisfait a => b = {w.satisfies(fIMP)}\"); // faux (a vrai, b faux)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**La localité de la satisfaction.** Toutes les réponses ci-dessus portent sur **un seul** monde\n",
"`w = [a]` : `satisfies` est une question *locale* (ce monde-ci, cette formule-ci). C'est la brique\n",
"atomique de toute la sémantique — les notions des sections suivantes ne sont que cette brique\n",
"*quantifiée* :\n",
"\n",
"- « modèle de F » = **il existe** un monde qui satisfait F ;\n",
"- « F valide » = **tous** les mondes satisfont F ;\n",
"- « KB |= b » = **tous** les mondes qui satisfont KB satisfont aussi b.\n",
"\n",
"Un bug de `satisfies` contamine donc toute la chaîne — d'où le soin de TweetyProject sur cette\n",
"méthode, et le test visuel facile : sur `w = [a]`, `b` doit échouer, `a||b` doit passer."
]
},
{
"cell_type": "markdown",
"id": "m5545",
Expand Down Expand Up @@ -466,6 +511,21 @@
"Console.WriteLine($\"Conjonction complete dans {{a,b,c}} = {w.getCompleteConjunction(sig)}\");\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Pourquoi une forme canonique ?** La sortie montre la correspondance terme à terme : chaque monde\n",
"possède **exactement une** conjonction complète (`[a, c]` ↔ `a&&c&&!b`). C'est une bijection monde ↔\n",
"formule — chaque monde de 2^n est *nommé* par une formule unique. Deux usages immédiats :\n",
"\n",
"- **non-ambiguïté** : deux formules différentes peuvent être équivalentes (`a&&b` vs `b&&a`), mais\n",
" deux conjonctions complètes distinctes désignent toujours des mondes distincts — le forme canonique\n",
" est l'identifiant du monde ;\n",
"- **passe-partout** : toute formule F s'écrit comme disjonction *exacte* des conjonctions complètes\n",
" de ses modèles (forme normale disjonctive pleine) — la base des compteurs de modèles."
]
},
{
"cell_type": "markdown",
"id": "m88739",
Expand Down Expand Up @@ -553,6 +613,21 @@
"Console.WriteLine($\"KB |= !a ? {r.query(kb, (PlFormula)p.parseFormula(\"!a\"))}\"); // faux : KB contient a\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**L'asymétrie de l'entailment.** Le verdict `KB |= b = true` ci-dessus a un coût de preuve\n",
"*dissymétrique* selon le sens :\n",
"\n",
"- **confirmer** exige de vérifier **tous** les modèles de KB (aucun contre-exemple) — coût 2^n ;\n",
"- **réfuter** suffit d'**un seul** monde contre-exemple (un modèle de KB où `b` échoue) — coût 1.\n",
"\n",
"C'est pourquoi le raisonnement automatique cherche toujours le contre-exemple d'abord : une seule\n",
"valuation réfutatrice tranche ce que l'énumération complète mettrait 2^n étapes à certifier. Le\n",
"`SatReasoner` de la cellule suit exactement cette stratégie (chercher un modèle de `KB ∧ ¬b`)."
]
},
{
"cell_type": "markdown",
"id": "m72867",
Expand Down Expand Up @@ -679,6 +754,20 @@
"Console.WriteLine($\"=> {models} modele(s) sur 8.\");\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Lecture des quatre survivants.** Sur les 8 mondes de `{a, b, c}`, exactement 4 restent : ceux où\n",
"l'heredité de la chaîne est respectée — jamais `a` sans `b`, jamais `b` sans `c`. Chacun des 4 mondes\n",
"exclus viole une flèche précise (`[a]`, `[a,b]` cassent `a=>b` ou `b=>c`...). Deux lectures utiles :\n",
"\n",
"- **généralisation** : énumérer les modèles de KB = filtrer la table de vérité sur les lignes qui\n",
" satisfont *toutes* les formules — la sémantique est un *filtre*, pas un calcul symbolique ;\n",
"- **comptage** : `4/8` est une mesure (le problème #SAT compte les modèles) — c'est la porte\n",
" d'entrée des sémantiques probabilistes : poser P uniforme sur les mondes et conditionner par KB."
]
},
{
"cell_type": "markdown",
"id": "m96153",
Expand Down Expand Up @@ -731,6 +820,20 @@
"Java minuscules). Rappel : les stubs doivent s'executer sans erreur (jamais `raise`/`assert`/`1/0`).\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Le protocole des exercices.** Les trois exercices rejouent les gestes des sections 2-4 en\n",
"montant en généralité : le premier classifie une formule (tautologie / contradiction / contingence) —\n",
"c'est une propriété **absolue**, indépendante de toute base ; le deuxième définit l'**équivalence\n",
"logique** comme double entailment (`F |= G` et `G |= F`) — un cas particulier de la section 4 ; le\n",
"troisième cherche une conséquence **cachée** d'une KB, là où l'intuition seule ne suffit plus. Les\n",
"squelettes sont exécutables tels quels (C.1) ; pour chacun, la stratégie gagnante est la même qu'en\n",
"cours : traduire la question en une requête sur les mondes, puis laisser l'énumérateur ou le\n",
"`SatReasoner` trancher."
]
},
{
"cell_type": "markdown",
"id": "m45853",
Expand All @@ -746,6 +849,24 @@
"comparer au total `2^n`.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Attendus, pour auto-vérification.** Avec la signature `{a, b}` (4 mondes), la classification se\n",
"lit directement sur l'énumération : une **tautologie** est vraie dans les 4 mondes (ex. `a||!a`), une\n",
"**contradiction** dans aucun (ex. `a&&!a`), une **contingence** dans certains seulement. Le réflexe à\n",
"institutionnaliser : *ne pas raisonner sur la formule, raisonner sur ses modèles* — la table des 4\n",
"mondes tranche toute question de ce niveau, sans calcul symbolique. Pour l'équivalence de l'exercice 2,\n",
"la double requête d'entailment doit donner **deux fois vrai** pour une équivalence réelle (et le\n",
"contre-exemple apparaît dès qu'un seul sens échoue : exhibez le monde réfutateur, pas juste\n",
"le booléen).\n",
"\n",
"Pour l'exercice 3, un conseil de méthode : listez d'abord à la main les modèles de la KB, puis\n",
"regardez quelles formules y sont vraies *partout* — la conséquence cachée est celle qui survit à ce\n",
"filtre sans être évidente à lire sur la syntaxe."
]
},
{
"cell_type": "code",
"execution_count": 10,
Expand Down
107 changes: 98 additions & 9 deletions MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-08-Agent-Dialogues-CSharp.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,6 @@
" The below script needs to be able to find the current output cell; this is an easy method to get it.\r\n",
" </div>\r\n",
" <script type='text/javascript'>\r\n",

" function timeout(ms, promise) {\r\n",
" return new Promise(function (resolve, reject) {\r\n",
" setTimeout(function () {\r\n",
Expand All @@ -67,10 +66,7 @@
" })\r\n",
" }\r\n",
"\r\n",


"\r\n",

"\r\n",
" if (!rootUrl.endsWith('/')) {\r\n",
" rootUrl = `${rootUrl}/`;\r\n",
Expand All @@ -85,7 +81,6 @@
" headers: {\r\n",
" 'Content-Type': 'text/plain'\r\n",
" },\r\n",

" }));\r\n",
"\r\n",
" if (response.status == 200) {\r\n",
Expand All @@ -97,8 +92,6 @@
" }\r\n",
"}\r\n",
"\r\n",


" .then((root) => {\r\n",
" // use probing to find host url and api resources\r\n",
" // load interactive helpers and language services\r\n",
Expand Down Expand Up @@ -147,13 +140,11 @@
" \r\n",
" \r\n",
" require_script.onload = function() {\r\n",

" };\r\n",
"\r\n",
" document.getElementsByTagName('head')[0].appendChild(require_script);\r\n",
"}\r\n",
"else {\r\n",

"}\r\n",
"\r\n",
" </script>\r\n",
Expand Down Expand Up @@ -347,6 +338,22 @@
"// Attendu : {D} (D defait C, donc C exclu ; sans C, A est attaquant ? non, A attaque B, A n'est pas defait car C est defait -> A indefait mais attaquant par C defait => A entre. Re-calculons.)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Lecture de l'extension grounded.** La sortie distingue acceptés (`D`, `A`) et rejetés implicitement\n",
"(`B`, `C` attaqués hors de l'extension). La sémantique **grounded** de Dung est la plus *prudente* :\n",
"elle part de l'ensemble vide et n'accepte un argument que s'il survit à toutes les attaques non\n",
"réfutées — construction par point fixe (d'abord les arguments sans attaquant, puis ceux qu'ils\n",
"défendent, etc.). Deux lectures du verdict affiché :\n",
"\n",
"- **sceptique par construction** : tout ce que grounded accepte, toutes les autres sémantiques\n",
" (préférée, stable) l'acceptent aussi — c'est le plancher commun ;\n",
"- **rejet ≠ faux** : `C` n'est pas « faux », il est *non défendable* dans cette théorie — changer une\n",
" seule attaque peut le réhabiliter (la Partie 4 le montrera en enrichissant l'AF)."
]
},
{
"cell_type": "markdown",
"id": "bf497e56-3021-422c-a715-7b419c404ac1",
Expand Down Expand Up @@ -467,6 +474,20 @@
"Show(antiAgent.Name + \" KB\", string.Join(\", \", antiAgent.Knowledge));\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Ce qui fait un agent « argumentatif ».** Le modèle ci-dessus tient en trois états : une **base de\n",
"connaissances** (ce que l'agent croit), un **stock d'engagements** (ce qu'il a *dit* — et dont il devra\n",
"répondre), et les **locutions** (`Claim`, `Argue`, `Concede`, `Retract`) comme seuls gestes de parole.\n",
"La distinction croire/dit est la clé : un agent peut être forcé de `Retract` un `Claim` attaqué sans\n",
"renier sa KB — il reconnaît avoir perdu *ce point-ci*, pas la guerre. C'est ce qui distingue un dialogue\n",
"argumentatif d'un échange d'opinions : chaque locution crée une **obligation vérifiable** (justifier un\n",
"`Claim` si on l'attaque), et le protocole peut rejeter un coup illégal — la rationalité est\n",
"procédurale, pas supposée."
]
},
{
"cell_type": "markdown",
"id": "a97fb4c4-6818-4cf4-ae8f-25323f477dbb",
Expand Down Expand Up @@ -593,6 +614,22 @@
"Show(\"Verdict\", $\"{outcome} — {why}\");\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Lecture de la trace — pourquoi Pro-TL gagne.** Le verdict `ProponentWins` vient d'un événement\n",
"précis : `Concede(le_teletravail_est_souhaitable)` au tour 2. Le protocole ne dit pas *comment* gagner\n",
"(il autorise les coups légaux), la stratégie de l'agent (quelle locution jouer) décide. Ici, Anti-TL\n",
"n'a pas su produire de contre-argument inattaquable — son unique attaque est contrée dans la KB adverse.\n",
"Deux observations :\n",
"\n",
"- le **résultat du dialogue** coïncide avec l'acceptation **grounded** de la thèse dans l'AF sous-jacent\n",
" — ce n'est pas un hasard : un dialogue bien formé est une *preuve interactive* de statut accepté ;\n",
"- un protocole sans règle de terminaison peut boucler (Claim/Retract indéfinis) — la limite de tours\n",
" du framework est une garde, pas un détail."
]
},
{
"cell_type": "markdown",
"id": "7d355049-86c2-4a1a-a641-cc4c524fd75c",
Expand Down Expand Up @@ -683,6 +720,19 @@
"Show(\"Verdict negociation\", $\"{o1} — {w1}\");\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Lecture du scénario d'achat.** L'AF `negociation` se lit comme un duel d'arguments immobiliers :\n",
"`COMP(comparables_bas)` et `UPG(travaux_prevus_deductibles)` ressortent acceptés par l'extension\n",
"grounded — le squelette de l'offre s'impose — pendant que `OVR` (prix haut vs marché) est attaqué.\n",
"Contrairement au débat télétravail, la négociation ici n'a qu'une **position initiale** de chaque côté :\n",
"la suite réelle d'une négociation (contre-offres, concessions conditionnelles) est précisément ce que\n",
"le protocole de dialogue de la Partie 3 outille — les locutions `Concede`/`Retract` sont les gestes de\n",
"la table de négociation."
]
},
{
"cell_type": "markdown",
"id": "998bee6d-c4d8-4288-8831-92cfa9f4e1d5",
Expand Down Expand Up @@ -769,6 +819,19 @@
"Show(\"Verdict teletravail\", $\"{o2} — {w2}\");\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Ce que l'enrichissement a changé.** Avant l'attaque `CT`, l'AF de la Partie 2 donnait la parole\n",
"aux pro-télétravail ; avec `CT(le_teletravail_isole_socialement)` et sa contre-attaque `S`, l'extension\n",
"grounded affichée intègre de nouveaux acceptés — la composition du débat a changé *sans qu'aucun\n",
"argument existant ne bouge*. Leçon structurelle : l'acceptation grounded est **globale** — ajouter un\n",
"argument n'importe où peut requalifier des arguments sans lien direct avec lui (via les chaînes\n",
"d'attaques). C'est la différence avec une base de croyances classique, où ajouter un fait ne retire\n",
"rien. Dans un débat réel : introduire un nouvel argument n'est jamais une opération locale."
]
},
{
"cell_type": "markdown",
"id": "0da7f67f-d0f4-441b-8e6b-d4861ad0775c",
Expand Down Expand Up @@ -870,6 +933,19 @@
"Show(\"Decision rationnelle\", uPro >= uAnti ? \"Pro-TL soutient le teletravail\" : \"Anti-TL s'oppose au teletravail\");\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Lecture de la décision.** Les espérances mesurées (`Pro-TL = 1,374` vs `Anti-TL = 0,731`) tranchent\n",
"en faveur du télétravail — mais il faut lire *ce que* la loterie évalue : chaque issue possible\n",
"(acceptation/rejet d'un argument) pondérée par sa croyance, chaque issue portant une utilité. La\n",
"décision est rationnelle **relativement aux utilités déclarées** — changez les poids (par ex. la\n",
"désutilité de l'isolement social `CT`) et le verdict peut basculer : c'est exactement le débat\n",
"politique réel, où les parties ne divergent souvent pas sur les faits mais sur les poids. Le calcul ne\n",
"remplace pas le choix de valeurs ; il le rend explicite et discutable."
]
},
{
"cell_type": "markdown",
"id": "c3feac81",
Expand Down Expand Up @@ -1131,6 +1207,19 @@
"Les exercices ci-dessous sont à compléter. Chaque stub s'exécute sans erreur (convention C.1) — remplacez le `TODO` par votre implémentation.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Le protocole des exercices.** Les trois exercices complètent le framework dans ses directions\n",
"naturelles : les **extensions préférées** (la sémantique crédulous — tout ensemble maximal admissible —\n",
"là où `grounded` était la plus prudente), un **tour de parole multi-agents** (généraliser le dialogue à\n",
"1-contre-1 de la Partie 3 en délibération à N), et l'**utilité exacte** de la Partie 5 (remplacer\n",
"l'espérance simulée par le calcul exact sur les extensions). Les squelettes sont exécutables tels quels\n",
"(C.1) ; chaque cellule annonce ce qu'elle doit afficher quand la solution est juste — ce sont vos\n",
"critères d'acceptation."
]
},
{
"cell_type": "code",
"execution_count": 9,
Expand Down
Loading
Loading