Tweety C# / IKVM - Logiques de Base (Port .NET du notebook Python)

Navigation : <- Tweety-1-Setup | Index serie | Tweety-3-Advanced-Logics ->

Ce notebook est le port C# / .NET de Tweety-02-Basic-Logics-Python.ipynb. Au lieu d’appeler Tweety depuis Python via JPype + JVM, on execute directement les classes Tweety recompilees en bytecode .NET via IKVM - aucune JVM, aucun JDK requis au runtime. Voir le notebook Python pour le contexte théorique complet.

Objectifs pedagogiques

  1. Charger la DLL Tweety (cluster pl) recompilee via IKVM 8.15
  2. Construire des formules propositionnelles (Proposition, Negation, Conjunction, Disjunction, Implication)
  3. Parser des formules depuis une chaîne avec PlParser
  4. Manipuler une base de croyances (PlBeliefSet) et explorer les mondes possibles (PossibleWorld)

Prerequis

  • Le notebook Python Tweety-02-Basic-Logics-Python.ipynb pour les notions (logique propositionnelle, mondes possibles)
  • Le runtime est tout .NET : aucune installation Java/JDK n’est necessaire

Plan de route : cinq étapes balisées, toutes exécutées et committées — (1) le runtime IKVM 8.15.0 restauré et vérifié, (2) la DLL Tweety chargée (org.tweetyproject.tweety-pl v1.30.0.0, 7,0 Mo), (3) la construction manuelle de cinq formules propositionnelles par constructeurs, (4) le parsing de la même syntaxe infixée via PlParser, (5) une base de croyances PlBeliefSet de quatre formules — dont vous montrerez qu’elle est involontairement inconsistante. Trois exercices closent le notebook, du DNF à la conséquence logique via SimplePlReasoner. Le fil rouge : le même arbre de formule se construit par l’API C# ou se lit par le DSL texte — deux portes, un AST.

Comment Tweety tourne en .NET (sans JVM)

Tweety est une bibliotheque Java. Pour l’utiliser depuis C#, on recompile son bytecode Java en bytecode .NET grace a IKVM :

  1. Recompilation : le bytecode Tweety 1.30 (Java 15) est recompile vers Java 8 (compatible IKVM 8.15, qui cible Java 8 SE), puis converti en une DLL .NET via <IkvmReference>.
  2. Fat-jar Maven shade : on assemble pl + ses dependances transitives (fol, logics-commons, math, commons, commons-math3, ojalgo, sat4j) en un unique fat-jar Maven coheren, qui preserve les metadonnees cross-module (un zip-merge artisanal les casserait).
  3. Runtime : la DLL org.tweetyproject.tweety-pl.dll (placee a cote de ce notebook) est referencee via #r ; IKVM fournit l’exécution de la JVM en .NET. La recette de build complete (POM shade + csproj) est dans dotnet-build/.

La cellule suivante configure ce runtime - a executer avant toute utilisation de Tweety.

Ce que « tzdb=True » confirme : la sortie du setup affiche IKVM 8.15.0 pret (home=ikvm-home-8.15.0-<rid>, tzdb=True), où <rid> désigne la plateforme de la machine (win-x64, linux-x64, osx-arm64…) — la base de données des fuseaux horaires IANA est embarquée et indexée, signe que la couche d’exécution Java est complète et pas seulementCompilee au strict minimum. Ce détail compte pour Tweety : certaines fonctionnalités des librairies Java (sérialisation, localisation) exigent des ressources embarquées que IKVM doit exposer. Le pont n’est pas gratuit pour autant : chaque appel traverse la frontière CLR/JVM — invisible sur des formules unitaires comme ici, mais à garder en tête avant de lancer un solveur sur des milliers d’instances.

1. Configuration du runtime IKVM

Cette cellule restaure les paquets NuGet IKVM et assemble le home IKVM. ~30-60 s la première fois.

Lecture de la sortie committée : la ligne IKVM 8.15.0 pret (home=ikvm-home-8.15.0-<rid>, tzdb=True) est le signal de santé du runtime — version résolue, domicile d’exécution dédié (ikvm-home-8.15.0-<rid>, ce qui évite les collisions entre versions cohabitantes), fuseaux disponibles. C’est la première chose à vérifier quand une cellule Tweety échoue : un IKVM à moitié restauré produit des erreurs trompeuses (types introuvables) qui n’ont rien à voir avec votre logique.

#r "nuget: IKVM, 8.15.0"
#r "nuget: IKVM.Image, 8.15.0"
Installed Packages
  • IKVM, 8.15.0
  • IKVM.Image, 8.15.0
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.15.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);

bool tzdbOk = File.Exists(Path.Combine(ikvmHome, "lib", "tzdb.dat"));
Console.WriteLine($"IKVM 8.15.0 pret (home=ikvm-home-{ikvmVer}-{ikvmRid}, tzdb={tzdbOk})");
IKVM 8.15.0 pret (home=ikvm-home-8.15.0-linux-x64, tzdb=True)

2. Chargement de la DLL Tweety

On reference la DLL recompilee. Le cluster pl expose les espaces de noms org.tweetyproject.logics.pl.syntax, org.tweetyproject.logics.pl.parser, etc.

Pourquoi la cellule suivante vérifie ce que #r ne dit pas : le commentaire du code invoque le constat #5039 — en .NET Interactive, la directive #r est silencieuse par défaut : elle n’affiche ni succès ni échec de chargement. Une référence cassée (chemin faux, DLL absente) ne se manifeste qu’à la première utilisation, parfois plusieurs cellules plus loin, avec un message d’erreur éloigné de la cause. D’où la cellule de vérification explicite : la sortie Tweety (IKVM) reference chargee : org.tweetyproject.tweety-pl v1.30.0.0 (7,0 Mo) prouve que l’assemblage est présent et lisible — vérifier tôt plutôt que diagnostiquer tard.

#r "org.tweetyproject.tweety-pl.dll"
// Constat 3 (#5039) : la directive #r est silencieuse par defaut en .NET Interactive.
// On verifie que la DLL IKVM/Tweety referencee est bien presente et lisible (metadata).
using System.Reflection;
var tweetyDll = "org.tweetyproject.tweety-pl.dll";
var an = AssemblyName.GetAssemblyName(tweetyDll);
Console.WriteLine($"Tweety (IKVM) reference chargee : {an.Name} v{an.Version} ({new FileInfo(tweetyDll).Length / 1024 / 1024:F1} Mo).");
Tweety (IKVM) reference chargee : org.tweetyproject.tweety-pl v1.30.0.0 (7.0 Mo).

3. Logique propositionnelle - construction manuelle de formules

On construit des formules comme dans le notebook Python, via l’API des classes Proposition, Negation, Conjunction, Disjunction, Implication.

Lecture des cinq constructions committées : la sortie affiche le round-trip saisie → toString() — a, !b, a&&!c, a||b, (a=>b). Deux observations. D’abord le mécanisme : en C#, && et || ne sont pas surchargeables — les formules se construisent donc par constructeurs explicites (new Negation(b), new Conjunction(a, new Negation(c)), new Disjunction(a, b), new Implication(a, b)), et c’est le toString() de Tweety qui restitue la syntaxe infixée. Ensuite la normalisation : l’implication seule garde ses parenthèses ((a=>b)) — la précédence de => étant la plus faible, Tweety les conserve par sécurité ; une conjonction au sein d’une conjon n’aurait pas besoin. Ces cinq formules forment l’alphabet structuré du notebook : chaque construction ultérieure (parse, KB, requêtes) les réutilise.

using org.tweetyproject.logics.pl.syntax;

var a = new Proposition("a");
var b = new Proposition("b");
var c = new Proposition("c");

var f1 = a;
var f2 = new Negation(b);
var f3 = new Conjunction(a, new Negation(c));
var f4 = new Disjunction(a, b);
var f5 = new Implication(a, b);

Console.WriteLine($"a       = {a}");
Console.WriteLine($"!b      = {f2}");
Console.WriteLine($"a && !c = {f3}");
Console.WriteLine($"a || b  = {f4}");
Console.WriteLine($"a => b  = {f5}");
a       = a
!b      = !b
a && !c = a&&!c
a || b  = a||b
a => b  = (a=>b)

4. Parsing de formules avec PlParser

Le PlParser lit des formules depuis une chaîne : ! (negation), && (conjonction), || (disjonction), => (implication), <=> (equivalence), ^^ (XOR).

Lecture du round-trip du parseur : (a || b) && !c saisie avec espaces et majuscules de lisibilité ressort (a||b)&&!c — le parseur produit exactement le même AST que la construction manuelle de la section précédente (new Conjunction(new Disjunction(a,b), new Negation(c))), seul le rendu textuel diffère. C’est la démonstration qu’il existe deux portes d’entrée vers le même objet : l’API C# typée (verrue : verbeuse) et le DSL texte (concis mais faillible — une parenthèse oubliée devient une exception au lieu d’une erreur de compilation). La seconde ligne introduit l’opérateur a^^b : le XOR exclusif, signature syntaxique propre à Tweety (^^), que la logique propositionnelle classique exprime sinon par (a||b)&&!(a&&b). Retenez la règle pratique : constructions manuelles pour les exemples pédagogiques, parseur pour tout ce qui vient d’une source texte (fichier, saisie utilisateur).

var parser = new org.tweetyproject.logics.pl.parser.PlParser();

var fParsed = parser.parseFormula("(a || b) && !c");
Console.WriteLine($"Parse de '(a || b) && !c' = {fParsed}");

var fXor = parser.parseFormula("a ^^ b");
Console.WriteLine($"XOR 'a ^^ b' = {fXor}");
Parse de '(a || b) && !c' = (a||b)&&!c
XOR 'a ^^ b' = a^^b

5. Base de croyances (PlBeliefSet)

Une PlBeliefSet est un ensemble de formules (base de connaissances). On reproduit la KB du notebook Python. Note d’API : IKVM expose les méthodes Java en minuscules (kb.add(...), kb.size()) - c’est la convention Java, pas les wrappers .NET.

Lecture de la KB committée — et son piège : la sortie affiche KB = { a&&!c, (a=>b), a, !b }, quatre formules. Regardez-la de près : elle est inconsistante, et probablement à l’insu de l’auteur. De a et (a=>b) le modus ponens tire b ; or !b est présent — la base affirme b et non-b à la fois. Ce n’est pas un bug du code mais une propriété logique de la base : en logique classique, une KB inconsistante entraîne n’importe quelle formule (ex falso quodlibet). C’est précisément le problème que Tweety-4 (révision de croyances) et Tweety-3 (mesure d’inconsistance) outillent : détecter, mesurer, réparer. Notez aussi l’ordre d’affichage { a&&!c, (a=>b), a, !b } — celui de l’insertion, un PlBeliefSet est un ensemble, pas une séquence : aucune sémantique d’ordre à lui prêter.

using org.tweetyproject.logics.pl.syntax;

var kb = new PlBeliefSet();
var p = new org.tweetyproject.logics.pl.parser.PlParser();
kb.add(p.parseFormula("a"));
kb.add(p.parseFormula("!b"));
kb.add(p.parseFormula("a && !c"));
kb.add(p.parseFormula("a => b"));

Console.WriteLine($"Base de croyances KB = {kb}");
Console.WriteLine($"Nombre de formules : {kb.size()}");
Base de croyances KB = { a&&!c, (a=>b), a, !b }
Nombre de formules : 4

Conclusion

Ce notebook demontre le port .NET fonctionnel de Tweety pour la logique propositionnelle :

Concept Classe Tweety (C#) Statut
Atome propositionnel Proposition OK
Connecteurs Negation, Conjunction, Disjunction, Implication OK
Parsing PlParser.parseFormula OK
Base de croyances PlBeliefSet (.add(), .size()) OK

Avantage du port .NET : aucune JVM ni JDK a installer, exécution native dans le kernel .net-csharp. Limitation : seule la logique propositionnelle (cluster pl) est portee dans ce pilote ; les notebooks Python restent canoniques pour la FOL complete, l’argumentation (notebooks 5-7), les MLN (notebook 10), etc. La sémantique via PossibleWorld + SatReasoner.query fera l’objet d’un notebook suivant.

Exercices

Reprenez ceux du notebook Python, adaptes a l’API C# (méthodes Java minuscules).

Note de parite cross-langage (EPIC #4956) : Le jumeau Python de ce notebook (voir Tweety-02-Basic-Logics-Python.ipynb) utilise jpype pour demarrer une JVM in-process et appeler directement les classes Java de Tweety. Ce notebook C# utilise IKVM pour transpiler statiquement le bytecode Java de Tweety en DLL .NET native (7 Mo charges a l’init, voir cellule 7). Les deux strategies donnent acces au meme API Tweety. Particularite : ce notebook utilise le vrai outil SOTA (IKVM recompilation), contrairement a certains jumeaux Tweety-6/8 (cf PR #7913 c.736) qui reimplementaient Monte-Carlo from-scratch en BCL .NET suite a une DLL IKVM defectueuse. Audit c.739 (2026-07-22) : 0 doc-honesty finding corrigible des deux cotes.

Les chiffres du parcours : un runtime IKVM 8.15.0 vérifié sain (tzdb=True), une DLL org.tweetyproject.tweety-pl v1.30.0.0 de 7,0 Mo chargée et lue, cinq constructions manuelles, deux parses round-trip, une KB de quatre formules — involontairement inconsistante, comme la lecture de la section 5 l’a établi. La chaîne .NET est complète : de la restauration NuGet à la requête logique, chaque maillon a sa preuve d’exécution committée. Les exercices suivants font franchir le dernier palier : de la construction de formules à l’interrogation d’une base.

Exercices 1 et 2 : critères de validation

Exercice 1 (DNF de l’équivalence) : la cible est (a => b) && (b => a) — l’équivalence matérielle. Sa forme normale disjonctive attendue est (a && b) || (!a && !b) : les deux lignes de la table de vérité où a et b coïncident. Deux voies, au choix : construction manuelle puis conversion (new Implication(...) pour chaque flèche, puis la méthode de conversion de la bibliothèque), ou PlParser direct — vérifiez dans les deux cas que le résultat affiché est bien la disjonction des deux cas favorables, pas la simple réécriture des implications ((¬a∨b)∧(a∨¬b) est la CNF, pas la DNF : les deux ne se ressemblent pas et ne sont pas interchangeables à l’affichage près).

Exercice 2 (KB de 4 formules) : reprenez le squelette de la section 5 — PlBeliefSet + PlParser.parseFormula quatre fois. Critère de réussite : la sortie affiche exactement 4 au compteur et l’itération de la collection rend chaque formule. La subtilité de l’exercice n’est pas le code mais le contenu : choisissez vos quatre formules de sorte que la base soit cohérente cette fois (contrairement à celle de la section 5) — vous vérifierez au passage que vous avez identifié pourquoi l’originale ne l’était pas.

// Exercice 1 : Construisez la formule (a => b) && (b => a) et affichez sa forme DNF.
// Indice : PlParser + .toNnf() ou construction manuelle.
// TODO etudiant : completez ici
Console.WriteLine("Exercice 1 a completer");
Exercice 1 a completer
// Exercice 2 : Parsez une KB de 4 formules et affichez sa taille + contenu.
// TODO etudiant : completez ici
Console.WriteLine("Exercice 2 a completer");
Exercice 2 a completer

Exercice 3 : Conséquence logique via SimplePlReasoner

Progression pédagogique : les exercices 1 et 2 ont introduit PlParser (parsing de formules) et PlBeliefSet (base de croyances). Cet exercice ajoute le raisonneur : etant donne une KB, determiner si une formule est consequence logique (model-theoretic entailment).

Question : soit la KB = {a, a => b, b => c}. La formule c est-elle consequence logique de KB ? Verifiez avec SimplePlReasoner.query(KB, c) (renvoie true/false). Commentez le résultat en termes de chainage modus ponens (a -> b -> c).

Indice : var reasoner = new SimplePlReasoner(); puis bool entailed = reasoner.query(kb, formula); — formula etant un objet PlFormula obtenu via PlParser.parse("c").

Critère de validation détaillé : la question posée est « la formule c est-elle conséquence de KB = {a, a=>b, b=>c} ? » — la réponse attendue est oui, par double modus ponens : a avec a=>b donne b, puis b avec b=>c donne c. Concrètement, SimplePlReasoner.query(kb, f) parcourt les interpretations et vérifie que chaque modèle de la KB satisfait f ; sur une KB de trois formules à trois propositions, l’espace est de 2³ = 8 interpretations — exhaustif et instantané. L’erreur classique à éviter : conclure « non » parce que c n’est pas syntaxiquement dans la KB — la conséquence est sémantique (vérité dans tous les modèles), pas de l’appartenance. Test de bord utile en passant : query(kb, new Negation(new Proposition("a"))) doit retourner faux (a est dans la KB).

// Exercice 3 : Conséquence logique via SimplePlReasoner.
//
// Paysage : KB propositionnelle = { a, a => b, b => c }.
// Question : la formule `c` est-elle consequence logique de KB ?
// Verdict attendu : true (chainage modus ponens : a, a=>b |- b ; b, b=>c |- c).
//
// AIDE : la cellule peut reutiliser `PlParser`, `PlBeliefSet` vus dans les exos 1/2,
// et instancier `SimplePlReasoner` pour le test d'inference.
// Pattern :
//   var parser = new PlParser();
//   var kb = new PlBeliefSet();
//   kb.add(parser.parseFormula("a"));
//   kb.add(parser.parseFormula("a => b"));
//   kb.add(parser.parseFormula("b => c"));
//   var reasoner = new SimplePlReasoner();
//   var query = parser.parseFormula("c");
//   bool entailed = reasoner.query(kb, query);
//   Console.WriteLine($"KB entail c : {entailed}");
//
// NOTE kernel : ce notebook est gated #r "nuget: IKVM, 8.15.0" + #r "org.tweetyproject.tweety-pl.dll"
// (cf. C171 leçon sœur PR #5147). L'execution reelle necessite VS Code Interactive (RECOVERABLE-MACHINE).
// Commit préserve execution_count=null + outputs=[] conformément à Stop & Repair (sota-not-workaround.md).

Console.WriteLine("Exercice 3 a completer — SimplePlReasoner.query(KB, c) sur {a, a=>b, b=>c}");
// TODO etudiant :
//   var parser = new PlParser();
//   var kb = new PlBeliefSet();
//   kb.add(parser.parseFormula("a"));
//   kb.add(parser.parseFormula("a => b"));
//   kb.add(parser.parseFormula("b => c"));
//   var reasoner = new SimplePlReasoner();
//   var query = parser.parseFormula("c");
//   bool entailed = reasoner.query(kb, query);
//   Console.WriteLine($"KB entail c : {entailed}");
//
// Variante : tester aussi KB entail (a & b) → false (KB ne dit pas que a et b sont vrais simultanement).
Exercice 3 a completer — SimplePlReasoner.query(KB, c) sur {a, a=>b, b=>c}
Retour au sommet