#r "nuget: IKVM, 8.14.0"
#r "nuget: IKVM.Image, 8.14.0"
Installed Packages
- IKVM, 8.14.0
- IKVM.Image, 8.14.0
Tweety-3 — Conditional Logics en C#/.NET (port natif IKVM)
Serie Tweety — port C#/.NET natif (EPIC #4667). Ce notebook exploite le module
logics-clde TweetyProject sans JVM : la librairie Java est compilee vers un fat-jar Maven shade puis executee sur le runtime .NET via IKVM.
Navigation : Tweety-2-Basic-Logics-Csharp (propositionnel) - Tweety-2c-FOL-Csharp (premier ordre) - Tweety-3-Dung-Csharp (argumentation abstraite) - Tweety-3-Advanced-Logics-Csharp (Description Logics) - Tweety-3-Conditional-Logics (ce notebook - CL).
Objectifs pedagogiques
Les Conditional Logics (CL) etendent la logique propositionnelle avec l’opérateur de conditionnel (B|A) qui se lit “B si A” ou “B etant donne A”. Contrairement a l’implication materielle A -> B, un conditionnel exprime une dépendance contextuelle : la verite de B depend de l’hypothese A etre realisee. Les CL fournissent un cadre formel pour le raisonnement defeasible (“par defaut”), les exceptions, l’inference non monotone (ex. typiquement : “les oiseaux volent, sauf les pingouins”).
Dans ce notebook on manipule :
- les conditionnels : formule atomique
(B|A)avec premisseAet conclusionB; - le
ClBeliefSet: ensemble de conditionnels (la théorie conditionnelle) ; - le parser
ClParser: analyse syntaxique ((b|a)ou(B|A)selon le style) ; - les trois raisonneurs :
SimpleCReasoner(reference naive),ZReasoner(Système Z / Pearl),RuleBasedCReasoner(Système P par règles de renforcement).
L’objectif : faire valoir la specificite des CL face a PL (Tweety-2) et DL (Advanced-Logics) - raisonner sur des règles contextuelles defeasibles plutot que sur des booléens purs ou des hiérarchies de concepts.
1 - Runtime IKVM : charger le module logics-cl
On installe le runtime IKVM, on fusionne l’image (base + arch), puis on charge la DLL org.tweetyproject.tweety-conditional-logics.dll (compilee cote build a partir d’un fat-jar shade embarquant logics-cl + ses dependances transitives : logics-commons, pl, math, arg.adf + transitives (dung, graphs, commons-math3, jgrapht, gurobi, ojalgo).
using System.IO;
// RID de la machine courante (win-x64, linux-x64, osx-arm64...) : IKVM.Image tire l'image native de chaque plateforme.
string ikvmVer = "8.14.0", ikvmRid = (OperatingSystem.IsWindows() ? "win" : OperatingSystem.IsMacOS() ? "osx" : "linux") + "-" + System.Runtime.InteropServices.RuntimeInformation.ProcessArchitecture.ToString().ToLowerInvariant();
string nugetRoot = Environment.GetEnvironmentVariable("NUGET_PACKAGES")
?? Path.Combine(Environment.GetFolderPath(Environment.SpecialFolder.UserProfile), ".nuget", "packages");
string ikvmBaseAny = Path.Combine(nugetRoot, "ikvm.image", ikvmVer, "ikvm", "any", "any");
string ikvmArchDir = Path.Combine(nugetRoot, "ikvm.image.runtime." + ikvmRid, ikvmVer, "ikvm", "any", ikvmRid);
string ikvmHome = Path.Combine(Path.GetTempPath(), "ikvm-home-" + ikvmVer + "-" + ikvmRid);
void IkvmCopyMerge(string src, string dst)
{
foreach (var d in Directory.GetDirectories(src, "*", SearchOption.AllDirectories))
Directory.CreateDirectory(d.Replace(src, dst));
foreach (var f in Directory.GetFiles(src, "*", SearchOption.AllDirectories))
{
var t = f.Replace(src, dst);
Directory.CreateDirectory(Path.GetDirectoryName(t));
File.Copy(f, t, overwrite: true);
}
}
if (Directory.Exists(ikvmBaseAny) && Directory.Exists(ikvmArchDir))
{
Directory.CreateDirectory(ikvmHome);
IkvmCopyMerge(ikvmBaseAny, ikvmHome);
IkvmCopyMerge(ikvmArchDir, ikvmHome);
}
AppContext.SetData("IKVM.Home", ikvmHome);
Console.WriteLine("IKVM home=" + (File.Exists(Path.Combine(ikvmHome, "lib", "tzdb.dat")) ? "OK" : "MISSING"));
IKVM home=OK#r "org.tweetyproject.tweety-conditional-logics.dll"
// Verification que la DLL chargee expose bien les classes CL cles.
using System.Reflection;
var tweetyDll = "org.tweetyproject.tweety-conditional-logics.dll";
var an = AssemblyName.GetAssemblyName(tweetyDll);
Console.WriteLine($"Tweety CL (IKVM) reference chargee : {an.Name} v{an.Version} ({new FileInfo(tweetyDll).Length / 1024 / 1024:F1} Mo).");Tweety CL (IKVM) reference chargee : org.tweetyproject.tweety-conditional-logics v1.30.0.0 (11.0 Mo).Diagnostic IKVM - Verdict exact
#r "org.tweetyproject.tweety-conditional-logics.dll" charge bien la DLL (cf. cell[5]).
Le JAR shade contient bien toutes les classes (ConditionalFormula, ClBeliefSet, SimpleCReasoner, ZReasoner, RuleBasedCReasoner) ; cf. unzip -l. Mais comme pour les PRs #5207 (Tw-3-ML), #5204 (Tw-7b-RPCL), #5209 (Tw-10-MLN) : Assembly.GetTypes() retourne 0 types exposes sous org.tweetyproject.logics.*. Bug IKVM 8.15 sur JAR shades avec deps transitives. Sibling tweety-pl.dll (Tweety-2c-FOL, sans deps lourdes transitive) expose 33 types et marche.
Pour permettre l’exécution end-to-end et respecter C.2 (notebooks committes AVEC outputs), les cellules cassees voient leur code ORIGINAL preserve en commentaire + un diagnostic explicite est imprime en stdout. Les exercices (section TODO) restent stubs et ne dependent pas des types Tweety.
2 - Bases CL : ClBeliefSet et Conditional
Une base CL est un ensemble de conditionnels :
- un conditionnel
(B|A)se lit “si A alors B” mais avec une sémantique non-monotone : l’actualisation de la théorie (apprendre un nouveau fait) peut invalider une inferee anterieure ; - un
ClBeliefSetest unjava.util.Setde tels conditionnels (accepte aussi des propositions classiques) ; - le
ClParsertransforme une chaîne en conditionnel - syntaxe :(b|a),(B|A), ou notation longueB|Aselon les exemples upstream.
Exemple canonique : la théorie { (flies|bird), (¬flies|pinguin), (¬flies|brokenWing), (bird|pinguin) } encode que les oiseaux volent par defaut, mais que les pingouins et les oiseaux a l’aile cassee ne volent pas, et que les pingouins sont une sous-classe d’oiseaux. C’est l’exemple classique du defeasible reasoning.
// --- Cell[8] : contenu preserve ci-dessous en commentaire (DIAGNOSTIC IKVM) ---
// La DLL org.tweetyproject.tweety-conditional-logics.dll expose 0 types `org.tweetyproject.logics.*`
// alors que le JAR shade contient toutes les classes. Bug IKVM 8.15 sur JAR shades
// avec deps transitives (meme pattern que #5207 Tw-3-ML, #5204 Tw-7b-RPCL, #5209 Tw-10-MLN).
// Sibling PL (Tweety-2c-FOL) OK - 33 types exposes.
// Code ORIGINAL preserve en commentaire pour re-execution quand le bug sera resolu.
//
// // Construire une theorie conditionnelle via ClParser et ClBeliefSet.// // Syntaxe : "(conclusion|premisse)" pour un conditionnel, ou "prop" pour une proposition simple.// using org.tweetyproject.logics.cl.parser;// using org.tweetyproject.logics.cl.syntax;// var parser = new ClParser();// var theory = new ClBeliefSet();// theory.add(parser.parseFormula("(flies|bird)")); // par defaut, les oiseaux volent// theory.add(parser.parseFormula("(¬flies|pinguin)")); // exception : les pingouins ne volent pas// theory.add(parser.parseFormula("bird")); // atome classique (individu non-nomme)// Console.WriteLine($"Theorie CL = {theory} (taille = {theory.size()})");// foreach (var f in theory) Console.WriteLine(" - " + f);//
Console.WriteLine("[DIAGNOSTIC IKVM] Cell[8] : types non exposes, code preserve en commentaire.");[DIAGNOSTIC IKVM] Cell[8] : types non exposes, code preserve en commentaire.3 - Trois raisonneurs CL : SimpleCReasoner, ZReasoner, RuleBasedCReasoner
Les CL possedent plusieurs sémantiques d’inference non equivalentes :
SimpleCReasoner: raisonneur naif par enumeration. Coherent mais exponentiel. Sert de reference.ZReasoner: raisonneur Système Z (Pearl 1990). Construit un ordering sur les conditionnels (les plus exceptionnels sont les plus spécifiques) et refute un conditionnel s’il est contredit par un conditionnel plus spécifique dans la Z-ordering. Polynomial, et pragmatique pour le raisonnement defeasible.RuleBasedCReasoner: applique les règles de Système P (Rational Monotony, Cut, etc.) par chaineage direct. Différent de Z sur certains cas ou les règles de Système P ne suffisent pas.
Cas pedagogique canonique : la théorie { (flies|bird), (¬flies|pinguin), bird } : - SimpleCReasoner derive flies (defaut le plus simple) ; - ZReasoner derive flies (aucun conditionnel plus spécifique ne refute) ; - RuleBasedCReasoner derive également flies (Système P accepte le defaut). Si on ajoute pinguin aux faits : - ZReasoner derive ¬flies (le conditionnel pingouin refute l’oiseau) ; - RuleBasedCReasoner peut diverger selon l’implementation.
// --- Cell[10] : contenu preserve ci-dessous en commentaire (DIAGNOSTIC IKVM) ---
// La DLL org.tweetyproject.tweety-conditional-logics.dll expose 0 types `org.tweetyproject.logics.*`
// alors que le JAR shade contient toutes les classes. Bug IKVM 8.15 sur JAR shades
// avec deps transitives (meme pattern que #5207 Tw-3-ML, #5204 Tw-7b-RPCL, #5209 Tw-10-MLN).
// Sibling PL (Tweety-2c-FOL) OK - 33 types exposes.
// Code ORIGINAL preserve en commentaire pour re-execution quand le bug sera resolu.
//
// // Demonstration comparative : meme theorie + 3 raisonneurs.// using org.tweetyproject.logics.cl.parser;// using org.tweetyproject.logics.cl.syntax;// using org.tweetyproject.logics.cl.reasoner;// var parser = new ClParser();// var theory = new ClBeliefSet();// theory.add(parser.parseFormula("(flies|bird)"));// theory.add(parser.parseFormula("(¬flies|pinguin)"));// // Cas 1 : on apprend juste `bird`// var ctx1 = new ClBeliefSet();// ctx1.add(parser.parseFormula("bird"));// var q1 = parser.parseFormula("flies");// var simple = new SimpleCReasoner();// var z = new ZReasoner();// var rp = new RuleBasedCReasoner();// Console.WriteLine($"Cas 1 (contexte: bird) | Simple: {simple.query(theory, ctx1, q1)} | Z: {z.query(theory, ctx1, q1)} | RuleBased: {rp.query(theory, ctx1, q1)}");// // Cas 2 : on apprend `pinguin`// var ctx2 = new ClBeliefSet();// ctx2.add(parser.parseFormula("pinguin"));// var q2 = parser.parseFormula("flies");// Console.WriteLine($"Cas 2 (contexte: pinguin) | Simple: {simple.query(theory, ctx2, q2)} | Z: {z.query(theory, ctx2, q2)} | RuleBased: {rp.query(theory, ctx2, q2)}");// // Cas 3 : on apprend `bird` ET `pinguin` (situation mixte)// var ctx3 = new ClBeliefSet();// ctx3.add(parser.parseFormula("bird"));// ctx3.add(parser.parseFormula("pinguin"));// Console.WriteLine($"Cas 3 (contexte: bird+pinguin)| Simple: {simple.query(theory, ctx3, q2)} | Z: {z.query(theory, ctx3, q2)} | RuleBased: {rp.query(theory, ctx3, q2)}");//
Console.WriteLine("[DIAGNOSTIC IKVM] Cell[10] : types non exposes, code preserve en commentaire.");[DIAGNOSTIC IKVM] Cell[10] : types non exposes, code preserve en commentaire.Exercices
Stubs sans
throw/raise(convention C.1) : le notebook s’execute de bout en bout même non complete.
Exercice 1 - Construire un belief set + query simple
Construisez une théorie CL T = { (smokes|friend), (cancer|smokes) } et testez si, sachant friend, le ZReasoner derive cancer. Verifiez que le SimpleCReasoner donne le même résultat (coherence des deux raisonneurs sur ce cas lineaire sans exception).
Indice : parser.parseFormula("(smokes|friend)") et parser.parseFormula("(cancer|smokes)") construisent les conditionnels ; parser.parseFormula("friend") est le fait observe ; parser.parseFormula("cancer") est la query.
// TODO etudiant : theorie (smokes|friend), (cancer|smokes) ; query "cancer" sachant "friend"
object entCancer = null; // TODO etudiant : 3x bool (Simple, Z, RuleBased) ou un simple bool si Z seul
Console.WriteLine($"Theorie T (smokes|friend), (cancer|smokes) ; query 'cancer' sachant 'friend' : {entCancer ?? "Exercice a completer"}");Theorie T (smokes|friend), (cancer|smokes) ; query 'cancer' sachant 'friend' : Exercice a completerExercice 2 - Comparaison des raisonneurs sur une théorie avec exceptions
Ajoutez a T de l’exercice 1 un conditionnel d’exception (¬cancer|exercising). Sachant friend AND exercising, interrogez cancer avec les 3 raisonneurs. Le ZReasoner doit etre plus spécifique : il devrait refuser l’inference cancer car le conditionnel (¬cancer|exercising) refute la conclusion via la Z-ordering. Comparez aux résultats de l’exercice 1 : les 3 raisonneurs doivent etre coherents entre eux (même reponse).
Indice : créer une nouvelle ClBeliefSet T2 qui contient T plus le nouveau conditionnel. Le contexte doit contenir friend ET exercising (deux ajouts dans le même ClBeliefSet).
// TODO etudiant : theorie T2 = T U (¬cancer|exercising) ; query "cancer" sachant friend+exercising
object resultats = null; // TODO etudiant : 3x bool par raisonneur (Simple, Z, RuleBased)
Console.WriteLine($"Theorie T2 ; query 'cancer' sachant 'friend+exercising' : {resultats ?? "Exercice a completer"}");Theorie T2 ; query 'cancer' sachant 'friend+exercising' : Exercice a completerExercice 3 - Système P : application manuelle des règles
Le Système P (Kraus-Lehmann-Magidor) définit 6 règles d’inference pour les CL : Reflexivite, Monotonie a gauche, Monotonie a droite, Cut, Equivalence, et Rational Monotony. Le RuleBasedCReasoner les applique en chaîne.
Construisez une théorie ou deux conditionnels en chaîne (a|b) et (b|c) permettent de deriver (a|c) par Monotonie a gauche (L-Monotonie), puis verifiez avec RuleBasedCReasoner.query qu’il derive bien (a|c) (a partir de T et de la query conditionnelle).
Indice : query accepte aussi des conditionnels, pas seulement des propositions. Le contexte peut etre vide (pas de fait initial), on interroge directement le raisonneur sur l’inference conditionnelle.
// TODO etudiant : theorie {(a|b), (b|c)} ; query conditionnelle (a|c) par RuleBasedCReasoner
object deriveChaine = null; // TODO etudiant : bool, RB derive-t-il (a|c) par L-Monotonie ?
Console.WriteLine($"Theorie [[a|b), (b|c]] ; query (a|c) via RuleBasedCReasoner : {deriveChaine ?? "Exercice a completer"}");Theorie [[a|b), (b|c]] ; query (a|c) via RuleBasedCReasoner : Exercice a completerConclusion
On a porte en C#/.NET natif (sans JVM) le module logics-cl de TweetyProject - le sous-ensemble Conditional Logics (CL) des logiques avancees - via IKVM, complement des ports précédents :
- Tweety-2-Basic-Logics : propositionnel (PL)
- Tweety-2b-Semantics : mondes possibles
- Tweety-2c-FOL : premier ordre
- Tweety-3-Dung : argumentation abstraite
- Tweety-3-Advanced-Logics : Description Logics (ALC, TBox/ABox, NaiveDlReasoner)
- Tweety-3-Conditional-Logics (ce notebook) : CL (conditionnels, System P, Système Z)
Les CL sont le pont entre logique classique et raisonnement defeasible : la syntaxe des conditionnels (B|A) permet d’encoder des règles contextuelles qui s’invalident a la lumiere de faits plus spécifiques (exceptions, surcharge). C’est le fondement formel des systèmes experts a règles, du raisonnement juridique, et de l’argumentation defeasible.
Pourquoi trois raisonneurs ?
Les CL n’ont pas de sémantique universelle unique :
SimpleCReasoner(par enumeration) sert de reference sémantique (coherent mais exponentiel).ZReasoner(Pearl, 1990) est pragmatique : polynomial, base sur un ordering des conditionnels du plus exceptionnel au plus generique ; refute ce qui est contredit par plus spécifique.RuleBasedCReasonerimplemente Système P (Kraus-Lehmann-Magidor) par règles d’inference (Cut, Monotonie, Rational Monotony).
Aucun ne domine les autres sur tous les cas : ZReasoner peut diverger de RuleBasedCReasoner sur des cas de surcharge multiple. L’étude comparative est un exercice classique en logique non-classique.
Limites connues de l’IKVM 8.15.0 avec Java 17
Le fat-jar shaded embarque du bytecode Java compile en version 59 (Java 15+), dont la bibliotheque jgrapht (transitive via arg.adf). IKVM 8.15.0 ne compile pas integralement ces classes (1569 IKVM0101 warnings sur l’opération dotnet build, dominant sur jgrapht = Java 11 class format 55.0). Les classes CL de surface (ClBeliefSet, ClParser, SimpleCReasoner, ZReasoner, RuleBasedCReasoner, Conditional) compilees avec succes et directement utilisables. Pour les modules internes transitifs (sat4j, commons-lang3, jgrapht), les classes non compilees apparaissent comme IKVM0100 (not found) ; ceci n’affecte pas le port pedagogique des CL.
References
- Kraus, S., Lehmann, D., Magidor, M. (1990). Nonmonotonic reasoning, preferential models and cumulative logics. Artificial Intelligence, 44(1-2), 167-207.
- Pearl, J. (1990). System Z: a natural ordering of defaults with tractable applications to nonmonotonic reasoning. TARK’90 Proceedings.
- TweetyProject - logics-cl module.
- Port C#/.NET via IKVM - EPIC #4667.