Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@
},
{
"cell_type": "markdown",
"id": "32384654",
"id": "f2310947",
"metadata": {
"papermill": {
"duration": 0.003408,
Expand All @@ -108,7 +108,20 @@
"- des **règles strictes** `premises -> conclusion` : deduction inattaquable (logique classique) ;\n",
"- des **règles defaisables** `premises => conclusion` : inference remise en cause (le coeur du debat).\n",
"\n",
"Une **formule** est une proposition (`d`) ou sa negation (`!d`). Deux formules sont **contradictoires** si l'une est la negation de l'autre : `Compl(d) = !d`, `Compl(!d) = d`.\n"
"Une **formule** est une proposition (`d`) ou sa negation (`!d`). Deux formules sont **contradictoires** si l'une est la negation de l'autre : `Compl(d) = !d`, `Compl(!d) = d`.\n",
"\n",
"### Pourquoi un axiome ne s'attaque pas\n",
"\n",
"Un axiome est une formule posee sans prerequis : aucune règle ne la conclut, donc **aucun argument ne peut la viser** — il n'existe pas de maillon amont a contester. C'est cette absence de prerequis, et non un statut privilegie accorde au texte, qui rend l'axiome inattaquable, et c'est pourquoi la théorie est representee en **trois champs separes** (axiomes, règles strictes, règles defaisables) plutot qu'en une liste unique de formules : le moteur a besoin de savoir, pour chaque formule, *par quelle sorte de règle* elle a été obtenue.\n",
"\n",
"### Ce que chaque sorte de règle expose a l'attaque\n",
"\n",
"| Sorte de règle | Son application | Sa conclusion |\n",
"|---|---|---|\n",
"| **Stricte** `p -> c` | inattaquable : la deduction est valide | attaquable si la conclusion est contredite |\n",
"| **Defaisable** `p => c` | attaquable (*undercut*) : on peut nier que la règle s'applique | attaquable (*rebut*) : on peut conclure le contraire |\n",
"\n",
"La difference n'est donc pas une nuance de degre, mais ce que l'attaquant peut viser. Les sections 2 et 3 ci-dessous n'exploitent que le **rebut** — une conclusion contre l'autre. L'*undercut* est laisse a l'exercice 2, qui etend le modele pour l'exprimer.\n"
]
},
{
Expand Down Expand Up @@ -178,7 +191,7 @@
},
{
"cell_type": "markdown",
"id": "c5233106",
"id": "abce5f68",
"metadata": {
"papermill": {
"duration": 0.003172,
Expand All @@ -198,7 +211,13 @@
"\n",
"On construit tous les arguments par **point fixe** : on part des axiomes, puis on applique iterativement toute règle dont les premisses sont déjà derivables, jusqu'a ne plus rien pouvoir ajouter.\n",
"\n",
"> Chaque conclusion n'etant ici produite que par une seule règle, on obtient exactement un argument par conclusion derivee (pas d'explosion combinatoire).\n"
"### Pourquoi un point fixe, et pas un parcours en profondeur\n",
"\n",
"L'ensemble des arguments d'une théorie est le plus petit ensemble **clos** par application des règles : un argument n'existe que si tous ses sous-arguments existent. Le point fixe calcule exactement cette cloture, et il la calcule **sans risque d'ordre** : partir des axiomes puis empiler les règles donne le meme ensemble que n'importe quel autre ordre d'application, puisque chaque etape n'ajoute que des arguments dont les premisses sont déjà la. Un parcours en profondeur, lui, devrait deviner par ou commencer et revisiter ses branches.\n",
"\n",
"La structure est **recursive** (un argument porte ses sous-arguments), ce qui est ce dont la generation d'attaques a besoin : attaquer un argument, c'est viser soit sa conclusion, soit une de ses premisses, et il faut pour cela pouvoir descendre dans l'arbre.\n",
"\n",
"> Chaque conclusion n'etant ici produite que par une seule règle, on obtient exactement un argument par conclusion derivee (pas d'explosion combinatoire). Ce n'est pas une propriete generale d'ASPIC+ : avec deux règles concluant la meme formule, on obtiendrait deux arguments distincts pour cette formule, et la cellule suivante devrait les distinguer.\n"
]
},
{
Expand Down Expand Up @@ -655,7 +674,7 @@
},
{
"cell_type": "markdown",
"id": "38510be6",
"id": "57bce6b5",
"metadata": {
"papermill": {
"duration": 0.003276,
Expand All @@ -673,7 +692,17 @@
"\n",
"La **tranche 2** qui suit est le pendant *production* : la meme theorie ASPIC+, mais traitee par la **lib Tweety reelle** (Java, via le pont IKVM). L'interet n'est pas de refaire ce que la tranche 1 fait deja, mais de **verifier la parite** : les deux moteurs doivent s'accorder sur le meme ensemble d'arguments, d'attaques et d'extensions. C'est la parite **jpype (Python) <=> IKVM (C#)** qui fait la valeur du jumeau C#.\n",
"\n",
"On reprend exactement la theorie de la section 3 (contradiction sur `d`) : deux axiomes `b, c`, trois regles defaisables `b,c => a`, `b => d`, `a => !d`."
"On reprend exactement la theorie de la section 3 (contradiction sur `d`) : deux axiomes `b, c`, trois regles defaisables `b,c => a`, `b => d`, `a => !d`.\n",
"\n",
"### Ce que le pont IKVM demande, concretement\n",
"\n",
"TweetyProject est une bibliotheque **Java** : pour l'appeler depuis .NET il faut un runtime Java *dans le processus*. Le pont IKVM (`IKVM`, `IKVM.Image`) fournit ce runtime sous forme de packages NuGet, et la mise en place prend trois gestes que les cellules suivantes executent :\n",
"\n",
"1. **declarer** les packages (`#r \"nuget: ...\"`) — l'image du runtime n'est pas livree avec le SDK .NET, elle est tiree a la demande ;\n",
"2. **assembler** un `IKVM.Home` : l'image se compose de deux packages, l'un **independant de la plateforme** et l'autre **specifique au RID** de la machine (`win-x64`, `linux-x64`, `osx-arm64`...). Les deux arborescences doivent etre fusionnees dans un meme repertoire avant que le runtime ne trouve ses fichiers ;\n",
"3. **charger** la DLL Java traduite (`org.tweetyproject.tweety-aspic.dll`) et verifier qu'elle est bien la.\n",
"\n",
"Le point delicat est que `#r` est **silencieux** : la directive n'echoue pas bruyamment quand la DLL manque, elle ne fait simplement rien. D'ou les cellules de verification ci-dessous : elles ne decryptent pas un resultat de calcul, elles **attestent que le pont est reellement en place** avant qu'on lui confie la theorie.\n"
]
},
{
Expand Down Expand Up @@ -804,6 +833,26 @@
"Console.WriteLine($\"Tweety (IKVM) charge : {an.Name} v{an.Version} ({new FileInfo(tweetyDll).Length / 1024 / 1024:F1} Mo).\");"
]
},
{
"cell_type": "markdown",
"id": "61eebebc",
"metadata": {
"papermill": {},
"tags": []
},
"source": [
"### Lecture : ce que le pont vient d'attester\n",
"\n",
"Les deux sorties se lisent comme un **cahier des charges satisfait**, pas comme un resultat d'argumentation :\n",
"\n",
"- `IKVM home=OK` — le test porte sur `lib/tzdb.dat`, un fichier **present dans le runtime Java lui-meme** et non dans la bibliotheque Tweety. Sa presence prouve que la fusion des deux packages (image neutre + image du RID) a produit une arborescence **complete** : si l'un des deux avait ete copie seul, `tzdb.dat` manquerait et le runtime echouerait au premier appel Java.\n",
"- `Tweety (IKVM) charge : org.tweetyproject.tweety-aspic v1.30.0.0 (8,0 Mo)` — la version et la taille sont lues par reflexion sur le fichier lui-meme (`AssemblyName.GetAssemblyName`), et non recopiees d'un commentaire : ce qui est affiche est ce qui est **sur le disque**. C'est la parade directe au silence de `#r` — on ne suppose pas que la DLL est la, on interroge son en-tete.\n",
"\n",
"Un mot sur ce que ces 8 Mo **sont** : une bibliotheque Java **traduite** en IL par IKVM, pas un processus Java lance a cote. L'appel a `AspicArgumentationTheory` plus bas s'executera donc **dans le processus .NET**, sans `java.exe` intermediaire ni pipe a serialiser — c'est ce qui rend la comparaison from-scratch <=> lib legitime : les deux moteurs tournent dans le meme espace d'execution, sur les memes objets, et l'ecart eventuel ne peut pas venir d'un probleme de transport.\n",
"\n",
"Cette mise en place est le **prealable** de la parite annoncee par le titre de la tranche : sans un pont verifie, un « meme resultat » ne prouverait rien, puisque rien ne garantirait que la lib ait seulement tourne.\n"
]
},
{
"cell_type": "markdown",
"id": "bc43479e",
Expand Down Expand Up @@ -1011,7 +1060,7 @@
},
{
"cell_type": "markdown",
"id": "63611905",
"id": "d61378a6",
"metadata": {
"papermill": {
"duration": 0.003884,
Expand All @@ -1025,7 +1074,13 @@
"source": [
"## Exercices (#2161)\n",
"\n",
"Trois exercices pour manipuler le moteur ASPIC+.\n"
"Trois exercices pour manipuler le moteur ASPIC+.\n",
"\n",
"Ils ne redemandent pas de relire le code : chacun casse une hypothese de la theorie de la section 3 et demande de **predire** ce que le moteur va faire avant de le lancer. Le premier reste dans le cadre du rebut, le deuxieme change le **type** d'attaque exprimable (c'est la vraie extension du modele), le troisieme sort d'ASPIC+ pour comparer avec un formalisme voisin.\n",
"\n",
"- **Exercice 1 — une quatrieme règle defaisable.** La theorie de la section 3 n'a qu'une seule source de conflit (`d` contre `!d`). Ajouter une regle, c'est ajouter des arguments *et* des attaques : la question a trancher est de savoir si le nouveau conflit est **resolu** ou s'il rejoint le cycle symetrique deja non resolu.\n",
"- **Exercice 2 — attaque *undercut*.** Jusqu'ici le moteur ne sait attaquer une **conclusion**. Viser l'**application** d'une règle demande d'etendre le modele de donnees, pas seulement d'ajouter une donnee : c'est le passage du rebut a l'undercut, et le meilleur moyen de mesurer ce qui manque au moteur de la section 2.\n",
"- **Exercice 3 — ASPIC+ face a ABA.** Les deux formalismes attaquent autre chose (une conclusion contre une hypothese) ; les mettre cote a cote sur un meme exemple demande de traduire la theorie dans les deux vocabulaires avant de comparer les extensions.\n"
]
},
{
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
date: '2026-10-10'
by: myia-po-2024:CoursIA-2
python_sha: bf64226ddaf769ac276e68c02cbf2ae8db05bd56
csharp_sha: 07f30095d9b7a8ae618d9bf968c2afdc6fef9b56
content_python_sha: 254f3dcf5c7088d614b009d4ef00f8856ecaefeaa446b9df8ead775f597d3bf4
content_csharp_sha: e8d45de7149bc530db38b3428025fac85af292c0ed4175038bc0956313e8179b
Loading