From 8a66cd945e6458167cd27a587308a07eb65a8139 Mon Sep 17 00:00:00 2001 From: jsboige Date: Thu, 17 Sep 2026 08:52:15 +0200 Subject: [PATCH 1/4] Add: 5 cellules markdown de lecture chiffree - SMT/Z3-API 13-UnsatCores (densite 1018 -> 1375) Edition md-only (11 cellules code byte-identiques vs aac9d62eb) : core de s0 = tout le systeme (chaque paire sat), minimalite verifiee dans les deux sens, relachements 8 vs 1 solutions, unicite du core 5/11 par l'arithmetique de la chaine (seul T3 viole, 8 > 7), deux preuves du meme UNSAT (core detaille 5 vs MUS transitif 3, -40 %). See #13410 Co-Authored-By: Claude Sonnet 5 --- .../SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb index 5ce9a3c3c7..abe372e2ed 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb @@ -119,6 +119,14 @@ "print(\"-> Z3 dit NON, mais ne dit pas (encore) POURQUOI.\")\n" ] }, + { + "cell_type": "markdown", + "id": "052d9b83", + "metadata": {}, + "source": [ + "**Lecture chiffree — un systeme ou le core serait TOUT.** `' a->b, a, !b ' : unsat` : le verdict brut tombe en une ligne. Mais ce petit systeme a une propriete que les exemples suivants n'auront pas : aucune de ses trois contraintes n'est superflue. Chaque paire prise seule est satisfiable — `{a->b, a}` tient avec `b` vrai, `{a->b, !b}` tient avec `a` faux, `{a, !b}` tient sans l'implication. Autrement dit, un core etiquete de ce systeme contiendrait les TROIS contraintes : le conflit nait de la combinaison complete, pas d'une paire. C'est la frontiere utile a connaitre avant la section suivante — l'etiquetage `assert_and_track` ne reduit que ce qui peut l'etre : quand chaque contrainte participe a la refutation, le core egale le systeme, et l'explication reste a ecrire a la main.\n" + ] + }, { "cell_type": "markdown", "id": "58f66f80", @@ -195,6 +203,14 @@ " print(\"-> Z3 ecarte 'x>=3' du core : cette contrainte est irrelevant pour le conflit.\")\n" ] }, + { + "cell_type": "markdown", + "id": "137659cb", + "metadata": {}, + "source": [ + "**Lecture chiffree — la minimalite verifiee dans les DEUX sens.** Core rendu : `x_le_5`, `x_eq_10` — la section 3 montrera que la paire suffit. L'autre sens est tout aussi testable et complete la definition : chaque membre du core pris individuellement est NECESSAIRE. Retirer `x_le_5` : `{x>=3, x=10}` est satisfiable (`x = 10` verifie les deux). Retirer `x_eq_10` : `{x>=3, x<=5}` est satisfiable (tout `x` de 3 a 5). Aucune des deux ne peut partir — le core est irreductible dans les deux directions : suffisant (paire UNSAT) et necessaire (chaque retrait redevient SAT). C'est la definition complete du MUS que la section 7 formalisera, deja realisee ici sur un exemple ou l'ecart se voit a l'oeil nu : `x = 10` est a 5 unites de la borne `x <= 5`.\n" + ] + }, { "cell_type": "markdown", "id": "09c603eb", @@ -346,6 +362,14 @@ " print(\" Action : relacher la contrainte 'h=12' (animateur) OU 'h!=12' (pause).\")\n" ] }, + { + "cell_type": "markdown", + "id": "8fad7629", + "metadata": {}, + "source": [ + "**Lecture chiffree — les deux relachements ne coutent pas le meme prix.** `Sur 5 contraintes, 2 seulement sont en conflit` — mais les deux manieres de guerir ne sont pas equivalentes, et le systeme restant les chiffre. Les trois contraintes innocentes bornent `h` dans l'intervalle [9, 17], soit 17 - 9 + 1 = 9 valeurs entieres. Relacher `h=12` (garder la pause dejeuner) : 9 - 1 = 8 solutions restent. Relacher `h!=12` (garder la demande de l'animateur) : exactement 1 solution, `h = 12`. Le core dit QUELLES contraintes sont en conflit ; compter ce que chaque relachement laisse voir est le pas supplementaire qui transforme le diagnostic en decision — ici, l'option pause dejeuner preserve 8 des 9 plannings possibles, l'option animateur en fige un seul.\n" + ] + }, { "cell_type": "markdown", "id": "a578ceff", @@ -498,6 +522,14 @@ "print(\"Contraintes innocentes ecartees (%d) : %s\" % (len(innocentes), \", \".join(innocentes)))" ] }, + { + "cell_type": "markdown", + "id": "21a44b5d", + "metadata": {}, + "source": [ + "**Lecture chiffree — pourquoi ce core de 5 est le SEUL possible.** `Taille du core : 5 contraintes sur 11`. L'arithmetique de la chaine explique a la fois le conflit et l'unicite. Les precedences imposent `start_T1 >= 2`, `start_T2 >= 4`, `start_T3 >= 6` (release de T0 puis +2 par tache) ; les deadlines exigent demarrer au plus a 5 — respecte avec marge pour T0 (2), T1 (4), T2 (6), viole seulement pour T3 (8 > 7). Il n'existe donc AUCUN autre chemin de conflit : retirer `release_T0` et la chaine flotte librement, retirer une precedence et la chaine se coupe, retirer `deadline_T3` et chaque echeance restante est tenable. Le core rendu n'est pas un choix parmi d'autres — c'est l'unique sous-ensemble irreductible, et les 6 contraintes ecartees le sont a bon droit.\n" + ] + }, { "cell_type": "markdown", "id": "0e0fd9dd", @@ -634,6 +666,14 @@ "print(\"-> Le core de Z3 (taille %d) n'etait PAS minimal : le MUS est de taille %d.\" % (len(core_z3), len(mus_labels)))\n" ] }, + { + "cell_type": "markdown", + "id": "3c987bed", + "metadata": {}, + "source": [ + "**Lecture chiffree — deux preuves differentes du meme UNSAT.** `Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5` puis `MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3`. Regarder les etiquettes, pas seulement les tailles : le core brut contient le chemin DETAILLE t0->t1->t2->t3, le MUS contient l'arete TRANSITIVE `e03` — absente du core. Deux preuves distinctes de la meme insatisfiabilite : Z3 refute en descendant la chaine (5+3+4 = 12, puis +2 = 14, contre la borne de 10), l'algorithme deletion-based trouve le raccourci et rend une preuve 40 % plus courte (3 contraintes contre 5). C'est le temoin concret de la lecon de la section 7 : le MUS n'est pas unique, et le core d'un meme systeme depend du chemin de refutation — avant de s'appuyer sur UN core pour relacher une contrainte, savoir qu'un autre existait, plus petit.\n" + ] + }, { "cell_type": "markdown", "id": "1d0cd879", From 1e8aa0dbc3b8e728488b8f469e7f8a8df9102f10 Mon Sep 17 00:00:00 2001 From: jsboige Date: Thu, 17 Sep 2026 09:25:43 +0200 Subject: [PATCH 2/4] Add: densite Argument_Analysis Ontology_Virtues - 4 lectures chiffrees (966 -> 1287) Tranche SymbolicAI/Argument_Analysis de l'EPIC densite #13410 : 4 cellules markdown de lecture chiffree inserees (echecs SOTA chiffres 848820/846857, recensement referme sur 2639, arithmetique d'arbre 223-1=222, concentration Walton 143/222). Edition md-only, 9 cellules code byte-identiques. See #13410 Co-Authored-By: Claude Sonnet 5 --- .../Argument_Analysis_Ontology_Virtues.ipynb | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argument_Analysis_Ontology_Virtues.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argument_Analysis_Ontology_Virtues.ipynb index 076b40cc0f..d2b59f23e4 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argument_Analysis_Ontology_Virtues.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argument_Analysis_Ontology_Virtues.ipynb @@ -145,6 +145,14 @@ "print(\" puis interrogation en SPARQL (le vrai outil SOTA opere sur le graphe RDF resultant).\")\n" ] }, + { + "cell_type": "markdown", + "id": "590f118e", + "metadata": {}, + "source": [ + "**Lecture chiffree — deux echecs differents, chiffres par le fichier lui-meme.** Le fichier pese `848,820 octets` pour `846,857 caracteres` de texte : 1,963 octets d'ecart, soit la somme des octets supplementaires des caracteres non ASCII (libelles accentues) une fois encodes en UTF-8. Face a lui, les deux outils SOTA echouent chacun de son cote : rdflib leve `parse direct impossible (TypeError)` — son parseur attend du RDF/XML — et owlready2 lit sans erreur mais `recompose 0 classe(s)` : le contenu SKOS n'est pas reconstruit. Un echec de format, un echec de reconstruction. Le pont de la cellule suivante ne contourne aucun moteur : il alimente le vrai, les requetes SPARQL sur un graphe rdflib.\n" + ] + }, { "cell_type": "code", "execution_count": 2, @@ -304,6 +312,14 @@ "print(\"Vertus (ce notebook) : thesaurus SKOS -- Concept + broader/narrower (hierarchie).\")\n" ] }, + { + "cell_type": "markdown", + "id": "19fe3418", + "metadata": {}, + "source": [ + "**Lecture chiffree — le recensement se referme sur le compte de construction.** La construction annoncait `Graphe SKOS construit : 2,639 triplets` ; la table des predicats, additionnee, rend exactement ce total : 446 + 446 + 410 + 224 + 223 + 222 + 222 + 222 + 222 + 1 + 1 = 2,639 — aucun triplet hors inventaire. Deux coherences de plus se lisent dans la meme table : `Concepts distincts (sujets) : 224` contre `Concepts (avec prefLabel) : 223` — le 224e sujet est le scheme lui-meme, qui n'est pas un concept mais porte l'unique `hasTopConcept` ; et le compte `rdf:type` monte aussi a 224 : chaque concept type, plus le scheme. Chaque ligne du recensement verifie le pont.\n" + ] + }, { "cell_type": "markdown", "id": "76ec68e5", @@ -417,6 +433,14 @@ " print(\" \" + \" -> \".join(path))\n" ] }, + { + "cell_type": "markdown", + "id": "a76989c5", + "metadata": {}, + "source": [ + "**Lecture chiffree — l'arithmetique d'un arbre.** `Concepts (avec prefLabel) : 223`, racine unique `validArgument`, et 222 relations `broader` : 223 - 1 = 222, la signature d'un arbre ou chaque concept non racine a exactement un parent — pas de DAG a heritage multiple. La racine affiche 7 `narrower` : exactement les 7 familles que l'ontologie s'attribue (`223 nodes, 7 families`), tandis que la tete la plus ramifiee, `simpleInference`, en compte 8 — une famille qui se subdivise. La lignee la plus profonde visible fait 4 sauts : de la feuille `absenceOfInternalContradictions` par `coherentDemonstration`, `correctDeductions` et `validReasoning` jusqu'a `validArgument`. Enfin 222 broader = 222 narrower : chaque lien hierarchique declare dans les deux sens, la convention SKOS sans exception.\n" + ] + }, { "cell_type": "markdown", "id": "e786ec67", @@ -614,6 +638,14 @@ "plt.show()\n" ] }, + { + "cell_type": "markdown", + "id": "ccdb8462", + "metadata": {}, + "source": [ + "**Lecture chiffree — la concentration du bon tenor.** `Schemes de Walton distincts portes par les vertus : 14`, et les 14 barres additionnees rendent le compte du recensement : 50 + 40 + 27 + 26 + 21 + 11 + 10 + 8 + 8 + 7 + 6 + 4 + 3 + 1 = 222, le total des liens `goodTenorOf`. La repartition est tres inegale : les quatre schemes de tete (Rule 50, Commitment 40, Bias 27, Sign 26) portent 143 vertus sur 222, soit environ 64 % ; a l'autre extremite, les sept moins productifs (8, 8, 7, 6, 4, 3, 1) totalisent 37 — moins que Rule seul. Des extremites 50 a 1 : le scheme Danger ne porte qu'une seule vertu. Le bon tenor se concentre ou les regles d'argumentation se declinent en nombreuses pratiques correctes.\n" + ] + }, { "cell_type": "markdown", "id": "6e503d32", From 6cf2af9343605c5134d843370d5cf0e68bbfbfbe Mon Sep 17 00:00:00 2001 From: jsboige Date: Thu, 17 Sep 2026 15:34:39 +0200 Subject: [PATCH 3/4] retract: remove Z3-Python-13-UnsatCores from this branch (delivered by #16514) The branch accidentally carried the full head of #16514 (Z3-13 grain, +40 lines) beneath the Ontology_Virtues commit, so the PR diff showed 2 files under a title that names only one. Restoring the file to its origin/main state makes the PR diff Ontology_Virtues-only and the stack merge-order independent (review 16515). Co-Authored-By: Claude Sonnet 5 --- .../SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb | 40 ------------------- 1 file changed, 40 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb index abe372e2ed..5ce9a3c3c7 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb @@ -119,14 +119,6 @@ "print(\"-> Z3 dit NON, mais ne dit pas (encore) POURQUOI.\")\n" ] }, - { - "cell_type": "markdown", - "id": "052d9b83", - "metadata": {}, - "source": [ - "**Lecture chiffree — un systeme ou le core serait TOUT.** `' a->b, a, !b ' : unsat` : le verdict brut tombe en une ligne. Mais ce petit systeme a une propriete que les exemples suivants n'auront pas : aucune de ses trois contraintes n'est superflue. Chaque paire prise seule est satisfiable — `{a->b, a}` tient avec `b` vrai, `{a->b, !b}` tient avec `a` faux, `{a, !b}` tient sans l'implication. Autrement dit, un core etiquete de ce systeme contiendrait les TROIS contraintes : le conflit nait de la combinaison complete, pas d'une paire. C'est la frontiere utile a connaitre avant la section suivante — l'etiquetage `assert_and_track` ne reduit que ce qui peut l'etre : quand chaque contrainte participe a la refutation, le core egale le systeme, et l'explication reste a ecrire a la main.\n" - ] - }, { "cell_type": "markdown", "id": "58f66f80", @@ -203,14 +195,6 @@ " print(\"-> Z3 ecarte 'x>=3' du core : cette contrainte est irrelevant pour le conflit.\")\n" ] }, - { - "cell_type": "markdown", - "id": "137659cb", - "metadata": {}, - "source": [ - "**Lecture chiffree — la minimalite verifiee dans les DEUX sens.** Core rendu : `x_le_5`, `x_eq_10` — la section 3 montrera que la paire suffit. L'autre sens est tout aussi testable et complete la definition : chaque membre du core pris individuellement est NECESSAIRE. Retirer `x_le_5` : `{x>=3, x=10}` est satisfiable (`x = 10` verifie les deux). Retirer `x_eq_10` : `{x>=3, x<=5}` est satisfiable (tout `x` de 3 a 5). Aucune des deux ne peut partir — le core est irreductible dans les deux directions : suffisant (paire UNSAT) et necessaire (chaque retrait redevient SAT). C'est la definition complete du MUS que la section 7 formalisera, deja realisee ici sur un exemple ou l'ecart se voit a l'oeil nu : `x = 10` est a 5 unites de la borne `x <= 5`.\n" - ] - }, { "cell_type": "markdown", "id": "09c603eb", @@ -362,14 +346,6 @@ " print(\" Action : relacher la contrainte 'h=12' (animateur) OU 'h!=12' (pause).\")\n" ] }, - { - "cell_type": "markdown", - "id": "8fad7629", - "metadata": {}, - "source": [ - "**Lecture chiffree — les deux relachements ne coutent pas le meme prix.** `Sur 5 contraintes, 2 seulement sont en conflit` — mais les deux manieres de guerir ne sont pas equivalentes, et le systeme restant les chiffre. Les trois contraintes innocentes bornent `h` dans l'intervalle [9, 17], soit 17 - 9 + 1 = 9 valeurs entieres. Relacher `h=12` (garder la pause dejeuner) : 9 - 1 = 8 solutions restent. Relacher `h!=12` (garder la demande de l'animateur) : exactement 1 solution, `h = 12`. Le core dit QUELLES contraintes sont en conflit ; compter ce que chaque relachement laisse voir est le pas supplementaire qui transforme le diagnostic en decision — ici, l'option pause dejeuner preserve 8 des 9 plannings possibles, l'option animateur en fige un seul.\n" - ] - }, { "cell_type": "markdown", "id": "a578ceff", @@ -522,14 +498,6 @@ "print(\"Contraintes innocentes ecartees (%d) : %s\" % (len(innocentes), \", \".join(innocentes)))" ] }, - { - "cell_type": "markdown", - "id": "21a44b5d", - "metadata": {}, - "source": [ - "**Lecture chiffree — pourquoi ce core de 5 est le SEUL possible.** `Taille du core : 5 contraintes sur 11`. L'arithmetique de la chaine explique a la fois le conflit et l'unicite. Les precedences imposent `start_T1 >= 2`, `start_T2 >= 4`, `start_T3 >= 6` (release de T0 puis +2 par tache) ; les deadlines exigent demarrer au plus a 5 — respecte avec marge pour T0 (2), T1 (4), T2 (6), viole seulement pour T3 (8 > 7). Il n'existe donc AUCUN autre chemin de conflit : retirer `release_T0` et la chaine flotte librement, retirer une precedence et la chaine se coupe, retirer `deadline_T3` et chaque echeance restante est tenable. Le core rendu n'est pas un choix parmi d'autres — c'est l'unique sous-ensemble irreductible, et les 6 contraintes ecartees le sont a bon droit.\n" - ] - }, { "cell_type": "markdown", "id": "0e0fd9dd", @@ -666,14 +634,6 @@ "print(\"-> Le core de Z3 (taille %d) n'etait PAS minimal : le MUS est de taille %d.\" % (len(core_z3), len(mus_labels)))\n" ] }, - { - "cell_type": "markdown", - "id": "3c987bed", - "metadata": {}, - "source": [ - "**Lecture chiffree — deux preuves differentes du meme UNSAT.** `Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5` puis `MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3`. Regarder les etiquettes, pas seulement les tailles : le core brut contient le chemin DETAILLE t0->t1->t2->t3, le MUS contient l'arete TRANSITIVE `e03` — absente du core. Deux preuves distinctes de la meme insatisfiabilite : Z3 refute en descendant la chaine (5+3+4 = 12, puis +2 = 14, contre la borne de 10), l'algorithme deletion-based trouve le raccourci et rend une preuve 40 % plus courte (3 contraintes contre 5). C'est le temoin concret de la lecon de la section 7 : le MUS n'est pas unique, et le core d'un meme systeme depend du chemin de refutation — avant de s'appuyer sur UN core pour relacher une contrainte, savoir qu'un autre existait, plus petit.\n" - ] - }, { "cell_type": "markdown", "id": "1d0cd879", From 559eab249a8c3969b1c2f76f1b52c56f464fceb7 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 20 Sep 2026 23:53:08 +0200 Subject: [PATCH 4/4] fix(argument-analysis,#13410): absorber 3 lectures chiffrees dans les lectures existantes (regle STOP #13410) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Une sortie a UNE cellule de lecture : les 3 cellules « Lecture chiffree » livrees (recensement, arithmetique de l'arbre, concentration goodTenorOf) etaient posees devant des lectures preexistantes des memes sorties. Contenu chiffre FUSIONNE dans les cellules preexistantes (RECRITES, registre accentue conserve, verbatim : 2639 triplets verifie par la somme des predicats, 223-1=222 arbre, 50+40+...+1=222), doublons supprimes. check_split_reading_cells.py -> clean. Delta net -40, markdown-only. Grain: MED/notebook-python -- lane myia-po-2026:CoursIA -- prev: MED/notebook-python #16507 Co-Authored-By: Claude Sonnet 5 --- .../Argument_Analysis_Ontology_Virtues.ipynb | 46 ++----------------- 1 file changed, 3 insertions(+), 43 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argument_Analysis_Ontology_Virtues.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argument_Analysis_Ontology_Virtues.ipynb index d2b59f23e4..f0201a1021 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argument_Analysis_Ontology_Virtues.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argument_Analysis_Ontology_Virtues.ipynb @@ -312,26 +312,12 @@ "print(\"Vertus (ce notebook) : thesaurus SKOS -- Concept + broader/narrower (hierarchie).\")\n" ] }, - { - "cell_type": "markdown", - "id": "19fe3418", - "metadata": {}, - "source": [ - "**Lecture chiffree — le recensement se referme sur le compte de construction.** La construction annoncait `Graphe SKOS construit : 2,639 triplets` ; la table des predicats, additionnee, rend exactement ce total : 446 + 446 + 410 + 224 + 223 + 222 + 222 + 222 + 222 + 1 + 1 = 2,639 — aucun triplet hors inventaire. Deux coherences de plus se lisent dans la meme table : `Concepts distincts (sujets) : 224` contre `Concepts (avec prefLabel) : 223` — le 224e sujet est le scheme lui-meme, qui n'est pas un concept mais porte l'unique `hasTopConcept` ; et le compte `rdf:type` monte aussi a 224 : chaque concept type, plus le scheme. Chaque ligne du recensement verifie le pont.\n" - ] - }, { "cell_type": "markdown", "id": "76ec68e5", "metadata": {}, "source": [ - "**Lecture** : le thesaurus compte **223 concepts** (chacun avec un `prefLabel`), **446\n", - "definitions** (223 x 2 langues), **222 relations `broader`** et autant de `narrower` -- la\n", - "double declaration est la convention SKOS (chaque lien hiérarchique est pose dans les deux\n", - "sens). Contrairement au pole sophismes, il n'y a **aucun** `NamedIndividual` ni\n", - "`ObjectPropertyAssertion` : la connaissance est portee par la **hiérarchie de concepts** et les\n", - "**annotations multilingues**, pas par un graphe de relations entre individus. Deux ontologies\n", - "soeurs, deux paradigmes : ABox relationnel pour les sophismes, thesaurus SKOS pour les vertus.\n" + "**Lecture** : le thesaurus compte **223 concepts** (chacun avec un `prefLabel`), **446 définitions** (223 x 2 langues), **222 relations `broader`** et autant de `narrower` -- la double declaration est la convention SKOS (chaque lien hiérarchique est posé dans les deux sens). Le recensement se referme sur le compte de construction : la construction annonçait `Graphe SKOS construit : 2,639 triplets` ; la table des prédicats, additionnée, rend exactement ce total : 446 + 446 + 410 + 224 + 223 + 222 + 222 + 222 + 222 + 1 + 1 = 2,639 -- aucun triplet hors inventaire. Deux cohérences de plus se lisent dans la même table : `Concepts distincts (sujets) : 224` contre 223 avec prefLabel -- le 224e sujet est le scheme lui-même, qui n'est pas un concept mais porte l'unique `hasTopConcept` ; et le compte `rdf:type` monte aussi à 224 : chaque concept typé, plus le scheme. Contrairement au pôle sophismes, il n'y a **aucun** `NamedIndividual` ni `ObjectPropertyAssertion` : la connaissance est portée par la **hiérarchie de concepts** et les **annotations multilingues**, pas par un graphe de relations entre individus. Deux ontologies sœurs, deux paradigmes : ABox relationnel pour les sophismes, thesaurus SKOS pour les vertus." ] }, { @@ -433,25 +419,12 @@ " print(\" \" + \" -> \".join(path))\n" ] }, - { - "cell_type": "markdown", - "id": "a76989c5", - "metadata": {}, - "source": [ - "**Lecture chiffree — l'arithmetique d'un arbre.** `Concepts (avec prefLabel) : 223`, racine unique `validArgument`, et 222 relations `broader` : 223 - 1 = 222, la signature d'un arbre ou chaque concept non racine a exactement un parent — pas de DAG a heritage multiple. La racine affiche 7 `narrower` : exactement les 7 familles que l'ontologie s'attribue (`223 nodes, 7 families`), tandis que la tete la plus ramifiee, `simpleInference`, en compte 8 — une famille qui se subdivise. La lignee la plus profonde visible fait 4 sauts : de la feuille `absenceOfInternalContradictions` par `coherentDemonstration`, `correctDeductions` et `validReasoning` jusqu'a `validArgument`. Enfin 222 broader = 222 narrower : chaque lien hierarchique declare dans les deux sens, la convention SKOS sans exception.\n" - ] - }, { "cell_type": "markdown", "id": "e786ec67", "metadata": {}, "source": [ - "**Lecture** : le concept racine est **`validArgument` (\"Argument valable\")** -- toute\n", - "vertu est une facette de l'argument valable. Les tetes de familles (`simpleInference`,\n", - "`thirdfigureSyllogism`, `acceptableInformalLogic`, `tangibleEvidence`, `credibleSources`...)\n", - "recouvrent les **7 familles** annoncees : logique formelle, logique informelle, qualite des\n", - "sources, des preuves, etc. La chaîne `broader` remonte de chaque feuille jusqu'a la racine :\n", - "c'est la profondeur du thesaurus, exploitable pour situer une vertu dans sa lignee.\n" + "**Lecture** : le concept racine est **`validArgument` (\"Argument valable\")** -- toute vertu est une facette de l'argument valable. L'arithmétique confirme un arbre : `Concepts (avec prefLabel) : 223`, racine unique, 222 relations `broader` -- 223 - 1 = 222, la signature d'un arbre où chaque concept non racine a exactement un parent, pas de DAG à héritage multiple. La racine affiche 7 `narrower` : exactement les 7 familles que l'ontologie s'attribue (`223 nodes, 7 families`), tandis que la tête la plus ramifiée, `simpleInference`, en compte 8 -- une famille qui se subdivise. La lignée la plus profonde visible fait 4 sauts : de la feuille `absenceOfInternalContradictions` par `coherentDemonstration`, `correctDeductions` et `validReasoning` jusqu'à `validArgument`. Les têtes de familles (`simpleInference`, `thirdfigureSyllogism`, `acceptableInformalLogic`, `tangibleEvidence`, `credibleSources`...) recouvrent les **7 familles** annoncées : logique formelle, logique informelle, qualité des sources, des preuves, etc. Et 222 broader = 222 narrower : chaque lien hiérarchique déclaré dans les deux sens, la convention SKOS sans exception. La chaîne `broader` remonte de chaque feuille jusqu'à la racine : c'est la profondeur du thesaurus, exploitable pour situer une vertu dans sa lignée." ] }, { @@ -638,25 +611,12 @@ "plt.show()\n" ] }, - { - "cell_type": "markdown", - "id": "ccdb8462", - "metadata": {}, - "source": [ - "**Lecture chiffree — la concentration du bon tenor.** `Schemes de Walton distincts portes par les vertus : 14`, et les 14 barres additionnees rendent le compte du recensement : 50 + 40 + 27 + 26 + 21 + 11 + 10 + 8 + 8 + 7 + 6 + 4 + 3 + 1 = 222, le total des liens `goodTenorOf`. La repartition est tres inegale : les quatre schemes de tete (Rule 50, Commitment 40, Bias 27, Sign 26) portent 143 vertus sur 222, soit environ 64 % ; a l'autre extremite, les sept moins productifs (8, 8, 7, 6, 4, 3, 1) totalisent 37 — moins que Rule seul. Des extremites 50 a 1 : le scheme Danger ne porte qu'une seule vertu. Le bon tenor se concentre ou les regles d'argumentation se declinent en nombreuses pratiques correctes.\n" - ] - }, { "cell_type": "markdown", "id": "6e503d32", "metadata": {}, "source": [ - "**Lecture** : les **14 schemes** de Walton relies aux vertus sont exactement ceux qui\n", - "apparaissent cote sophismes. Les plus productifs -- *Argument from Rule* (50 vertus), *from\n", - "Commitment* (40), *from Bias* (27), *from Sign* (26) -- sont les schemes ou l'argumentation\n", - "correcte se decline en de nombreuses bonnes pratiques. La propriete `goodTenorOf` est donc le\n", - "**pivot** qui permettra, dans les exercices, de relier une vertu a son sophisme miroir via le\n", - "schema partage.\n" + "**Lecture** : les **14 schemes** de Walton reliés aux vertus sont exactement ceux qui apparaissent côté sophismes. `Schemes de Walton distincts portés par les vertus : 14`, et les 14 barres additionnées rendent le compte du recensement : 50 + 40 + 27 + 26 + 21 + 11 + 10 + 8 + 8 + 7 + 6 + 4 + 3 + 1 = 222, le total des liens `goodTenorOf`. La répartition est très inégale : les quatre schemes de tête -- *Argument from Rule* (50 vertus), *from Commitment* (40), *from Bias* (27), *from Sign* (26) -- portent 143 vertus sur 222 (environ 64 %), là où l'argumentation correcte se décline en nombreuses bonnes pratiques ; à l'autre extrémité, les sept moins productifs (8, 8, 7, 6, 4, 3, 1) totalisent 37 -- moins que Rule seul -- et le scheme Danger ne porte qu'une seule vertu. La propriété `goodTenorOf` est donc le **pivot** qui permettra, dans les exercices, de relier une vertu à son sophisme miroir via le schéma partagé." ] }, {