Tweety C# / IKVM - Sémantique propositionnelle : mondes possibles et raisonnement

Navigation : <- Tweety-2-Basic-Logics | Index serie | Tweety-3-Advanced-Logics ->

Ce notebook est le second volet C# / .NET de la serie Tweety. Il poursuit Tweety-2-Basic-Logics-Csharp (construction de formules, parsing, base de croyances) en abordant la sémantique : mondes possibles, satisfaction, et raisonnement (entaînement). Comme le pilote, il execute les classes Tweety recompilees en bytecode .NET via IKVM - aucune JVM au runtime. Voir le notebook Python pour le contexte théorique complet.

Objectifs pedagogiques

  1. Construire une signature propositionnelle (PlSignature) et enumerer ses mondes possibles (PossibleWorldIterator)
  2. Tester la satisfaction d’une formule par un monde (PossibleWorld.satisfies)
  3. Effectuer du raisonnement : une base de croyances entaîne-t-elle une formule ? (SatReasoner.query)
  4. Relier l’approche sémantique (enumeration des modèles) et l’approche syntaxique (solveur SAT)

Prerequis

  • Tweety-2-Basic-Logics-Csharp (construction de formules, PlBeliefSet, PlParser)
  • Notions de logique propositionnelle : valuation, modèle, consequence logique

Rappel d’API (C# / IKVM) : les classes Java Tweety sont exposees via IKVM avec la convention Java minuscule (.add(), .size(), .hasNext()…). Le PlParser.parseFormula() retourne le type de base commons.Formula ; on le cast en PlFormula pour les méthodes sémantiques.

1. Configuration du runtime IKVM

Identique au pilote : on restaure les paquets NuGet IKVM, on assemble le home IKVM (motrice d’exécution de la JVM en .NET), puis on charge la DLL Tweety. A executer en premier. ~30-60 s la première fois.

#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)
#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).

Pourquoi un pont Java→.NET ? Les cellules de configuration ci-dessus chargent la bibliothèque TweetyProject — écrite en Java — dans le processus .NET, via IKVM (une réimplémentation du runtime Java en bytecode .NET). Le choix pédagogique est assumé : TweetyProject est l’implémentation de référence des logiques pour agents (argumentation, croyances, préférences), maintenue et testée par la communauté ; la réécrire « pour faire C# » perdrait ce référentiel. Le pont rend les deux mondes comparables : même signature, mêmes mondes, mêmes verdicts — et le jour où un twin C# from-scratch existe pour un module, la parité se mesure contre cette référence au lieu d’être supposée.

2. Signature et mondes possibles

Une signature propositionnelle (PlSignature) est l’ensemble des atomes (propositions) du langage. Pour n atomes, il existe 2^n mondes possibles (valuations) : chaque atome peut etre vrai ou faux. Un monde possible (PossibleWorld) est l’ensemble des atomes consideres comme vrais (les autres etant faux par complement).

Le PossibleWorldIterator enumerera automatiquement tous les mondes d’une signature.

Exemple : signature {a, b} -> 4 mondes : [] (aucun), [a], [b], [a, b].

using org.tweetyproject.logics.pl.syntax;
using org.tweetyproject.logics.pl.semantics;
using org.tweetyproject.logics.pl.parser;

var p = new PlParser();
var sig = new PlSignature();
sig.add(p.parseFormula("a"));
sig.add(p.parseFormula("b"));

Console.WriteLine($"Signature : {sig}");

Console.WriteLine("Mondes possibles :");
int n = 0;
var it = new PossibleWorldIterator(sig);
while (it.hasNext())
{
    var world = (PossibleWorld) it.next();
    Console.WriteLine($"  monde {n} = {world}");
    n++;
}
Console.WriteLine($"=> {n} mondes pour 2 atomes (2^2 = 4).");
Signature : [a, b]
Mondes possibles :
  monde 0 = []
  monde 1 = [a]
  monde 2 = [b]
  monde 3 = [a, b]
=> 4 mondes pour 2 atomes (2^2 = 4).

Interpretation : mondes possibles et sémantique

Chaque monde correspond a une interpretation (valuation de verite) : {a} signifie a est vrai, b est faux ; le monde vide [] = tous les atomes faux. L’itération couvre exhaustivement les 2^n cas de la table de verite — c’est la base de la sémantique de Tarski : une formule est vraie dans un monde si sa valuation la satisfait.

La structure des mondes. Les quatre mondes affichés ne sont pas une liste plate : ordonnés par inclusion ([] ⊂ [a] ⊂ [a,b]), ils forment le cube B_n — l’hypercube des valuations (pour 2 atomes, un carré ; pour n, un n-cube). Deux propriétés de cette structure servent toute la suite :

  • le monde vide [] et le monde plein [a,b] sont les deux extrêmes (tout-faux / tout-vrai) ;
  • les formules monotones (sans négation d’atome) décrivent des up-sets du cube — leur ensemble de modèles est stable par ajout d’atomes. Les requêtes des sections 3-4 se lisent alors géométriquement : intersecter des up-sets, chercher des contre-exemples en descendant.

3. Satisfaction : un monde est-il modèle d’une formule ?

La méthode PossibleWorld.satisfies(PlFormula) repond : ce monde rend-il la formule vraie ? Une formule est satisfiable s’il existe au moins un monde qui la satisfait ; elle est une tautologie si tous les mondes la satisfont ; elle est une contradiction si aucun monde ne la satisfait.

On construit un monde en lui ajoutant des Proposition (les atomes vrais), puis on teste la satisfaction. Notez le cast (PlFormula) : parseFormula retourne le type generique Formula, que les méthodes sémantiques precisent en PlFormula.

using org.tweetyproject.logics.pl.syntax;
using org.tweetyproject.logics.pl.semantics;
using org.tweetyproject.logics.pl.parser;

var p = new PlParser();

// Un monde ou a=vrai, b=faux
var w = new PossibleWorld();
w.add(new Proposition("a"));
Console.WriteLine($"Monde w = {w}");

var fa   = (PlFormula) p.parseFormula("a");
var fb   = (PlFormula) p.parseFormula("b");
var fAND = (PlFormula) p.parseFormula("a && b");
var fOR  = (PlFormula) p.parseFormula("a || b");
var fIMP = (PlFormula) p.parseFormula("a => b");

Console.WriteLine($"  w satisfait a      = {w.satisfies(fa)}");   // vrai  (a dans w)
Console.WriteLine($"  w satisfait b      = {w.satisfies(fb)}");   // faux  (b absent)
Console.WriteLine($"  w satisfait a && b = {w.satisfies(fAND)}"); // faux  (b absent)
Console.WriteLine($"  w satisfait a || b = {w.satisfies(fOR)}");  // vrai  (a vrai)
Console.WriteLine($"  w satisfait a => b = {w.satisfies(fIMP)}"); // faux  (a vrai, b faux)
Monde w = [a]
  w satisfait a      = True
  w satisfait b      = False
  w satisfait a && b = False
  w satisfait a || b = True
  w satisfait a => b = False

La localité de la satisfaction. Toutes les réponses ci-dessus portent sur un seul monde w = [a] : satisfies est une question locale (ce monde-ci, cette formule-ci). C’est la brique atomique de toute la sémantique — les notions des sections suivantes ne sont que cette brique quantifiée :

  • « modèle de F » = il existe un monde qui satisfait F ;
  • « F valide » = tous les mondes satisfont F ;
  • « KB |= b » = tous les mondes qui satisfont KB satisfont aussi b.

Un bug de satisfies contamine donc toute la chaîne — d’où le soin de TweetyProject sur cette méthode, et le test visuel facile : sur w = [a], b doit échouer, a||b doit passer.

Representation canonique d’un monde

La méthode getCompleteConjunction(PlSignature) produit la conjonction complete representant un monde dans une signature donnee (un litteral positif par atome vrai, negatif par atome faux). C’est la forme normale disjonctive canonique d’une valuation.

using org.tweetyproject.logics.pl.syntax;
using org.tweetyproject.logics.pl.semantics;
using org.tweetyproject.logics.pl.parser;

var p = new PlParser();
var sig = new PlSignature();
sig.add(p.parseFormula("a"));
sig.add(p.parseFormula("b"));
sig.add(p.parseFormula("c"));

// Monde {a, c} dans la signature {a, b, c}
var w = new PossibleWorld();
w.add(new Proposition("a"));
w.add(new Proposition("c"));
Console.WriteLine($"Monde = {w}");
Console.WriteLine($"Conjonction complete dans {{a,b,c}} = {w.getCompleteConjunction(sig)}");
Monde = [a, c]
Conjonction complete dans {a,b,c} = a&&c&&!b

Pourquoi une forme canonique ? La sortie montre la correspondance terme à terme : chaque monde possède exactement une conjonction complète ([a, c] ↔︎ a&&c&&!b). C’est une bijection monde ↔︎ formule — chaque monde de 2^n est nommé par une formule unique. Deux usages immédiats :

  • non-ambiguïté : deux formules différentes peuvent être équivalentes (a&&b vs b&&a), mais deux conjonctions complètes distinctes désignent toujours des mondes distincts — le forme canonique est l’identifiant du monde ;
  • passe-partout : toute formule F s’écrit comme disjonction exacte des conjonctions complètes de ses modèles (forme normale disjonctive pleine) — la base des compteurs de modèles.

4. Raisonnement : consequence logique (entaînement)

Enumerer les mondes est exact mais couteux (2^n). Pour le raisonnement - une base de croyances KB entaîne-t-elle une formule phi (note KB |= phi) ? - on delegue a un solveur SAT interne (Sat4j) via SatReasoner.query(PlBeliefSet, PlFormula).

Principe : KB |= phi ssi il n’existe aucun modèle de KB qui falsifie phi. Le solveur verifie cela sans enumerer exhaustivement. La méthode retourne un booléen.

Exemple : avec KB = { a, a => b }, on a KB |= b (modus ponens) mais KB |= c est faux.

using org.tweetyproject.logics.pl.syntax;
using org.tweetyproject.logics.pl.reasoner;
using org.tweetyproject.logics.pl.parser;

var p = new PlParser();
var kb = new PlBeliefSet();
kb.add(p.parseFormula("a"));
kb.add(p.parseFormula("a => b"));
Console.WriteLine($"KB = {kb}");

var r = new SatReasoner();
Console.WriteLine($"KB |= b    ? {r.query(kb, (PlFormula)p.parseFormula("b"))}");      // vrai  : modus ponens
Console.WriteLine($"KB |= c    ? {r.query(kb, (PlFormula)p.parseFormula("c"))}");      // faux  : c non derive
Console.WriteLine($"KB |= a||c ? {r.query(kb, (PlFormula)p.parseFormula("a || c"))}"); // vrai  : a vrai => disjonction
Console.WriteLine($"KB |= !a   ? {r.query(kb, (PlFormula)p.parseFormula("!a"))}");     // faux  : KB contient a
KB = { (a=>b), a }
KB |= b    ? true
KB |= c    ? false
KB |= a||c ? true
KB |= !a   ? false

Interpretation : l’asymétrie et les deux approches

L’asymétrie de l’entailment. Le verdict KB |= b = true ci-dessus a un coût de preuve dissymétrique selon le sens :

  • confirmer exige de vérifier tous les modèles de KB (aucun contre-exemple) — coût 2^n ;
  • réfuter suffit d’un seul monde contre-exemple (un modèle de KB où b échoue) — coût 1.

C’est pourquoi le raisonnement automatique cherche toujours le contre-exemple d’abord. Deux approches équivalentes pour KB |= phi :

  • Sémantique (énumérateur) : parcourir tous les modèles de KB et vérifier que chacun satisfait phi — exact mais coût 2^n ;
  • Syntaxique (solveur SAT) : tester la (in)satisfiabilité de KB et non phi — s’il n’y a pas de modèle, phi est conséquence. C’est exactement la stratégie du SatReasoner (DPLL/CDCL via Sat4j), bien plus efficace dès que n grandit — le cœur des moteurs modernes de raisonnement.

Exemple guide : modèles d’une base de croyances

Croisons les deux approches : trouvons les mondes qui satisfont toute la KB (ses modèles). Un monde est modèle de KB s’il satisfait chaque formule. PossibleWorld.satisfies accepte directement un PlBeliefSet.

using org.tweetyproject.logics.pl.syntax;
using org.tweetyproject.logics.pl.semantics;
using org.tweetyproject.logics.pl.parser;

var p = new PlParser();
var kb = new PlBeliefSet();
kb.add(p.parseFormula("a => b"));   // si a alors b
kb.add(p.parseFormula("b => c"));   // si b alors c
Console.WriteLine($"KB = {kb}");

// Signature {a, b, c} -> 8 mondes ; on filtre ceux qui sont modeles de KB
var sig = new PlSignature();
sig.add(p.parseFormula("a"));
sig.add(p.parseFormula("b"));
sig.add(p.parseFormula("c"));

Console.WriteLine("Modeles de KB :");
int models = 0;
var it = new PossibleWorldIterator(sig);
while (it.hasNext())
{
    var world = (PossibleWorld) it.next();
    if (world.satisfies(kb))
    {
        Console.WriteLine($"  {world}  -> conjonction complete : {world.getCompleteConjunction(sig)}");
        models++;
    }
}
Console.WriteLine($"=> {models} modele(s) sur 8.");
KB = { (a=>b), (b=>c) }
Modeles de KB :
  []  -> conjonction complete : !a&&!b&&!c
  [c]  -> conjonction complete : c&&!a&&!b
  [b, c]  -> conjonction complete : b&&c&&!a
  [a, b, c]  -> conjonction complete : a&&b&&c
=> 4 modele(s) sur 8.

Lecture des quatre survivants. Sur les 8 mondes de {a, b, c}, exactement 4 restent : ceux où l’hérité de la chaîne est respectée — jamais a sans b, jamais b sans c. Chacun des 4 mondes exclus viole une flèche précise ([a], [a,b] cassent a=>b ou b=>c…). KB impose c dès que a est vrai (chaînage a => b => c) : c’est exactement la fermeture transitive des implications, vue sémantiquement.

Deux lectures utiles :

  • généralisation : énumérer les modèles de KB = filtrer la table de vérité sur les lignes qui satisfont toutes les formules — la sémantique est un filtre, pas un calcul symbolique ;
  • comptage : 4/8 est une mesure (le problème #SAT compte les modèles) — c’est la porte d’entrée des sémantiques probabilistes : poser P uniforme sur les mondes et conditionner par KB.

Le lien profond se referme ici : KB |= phi équivaut à « phi est vraie dans tous les modèles de KB » — le théorème de Tarski déjà entrevu en section 3 (quantification de la brique satisfies).

Conclusion

Ce notebook complete le pilote Tweety-2-Basic-Logics-Csharp avec la sémantique de la logique propositionnelle en .NET natif :

Concept Classe Tweety (C#) Méthode Statut
Signature PlSignature .add() OK
Monde possible PossibleWorld .add(Proposition), .satisfies() OK
Enumeration des mondes PossibleWorldIterator .hasNext(), .next() OK
Conjonction complete PossibleWorld .getCompleteConjunction(sig) OK
Raisonnement (entaînement) SatReasoner .query(PlBeliefSet, PlFormula) OK

Deux approches equivalentes : enumeration sémantique (2^n) pour la pedagogie, solveur SAT (Sat4j) pour l’efficacite. Le port .NET couvre desormais la construction et le raisonnement de la logique propositionnelle, sans JVM.

Limitation

Comme le pilote, ce notebook porte uniquement le cluster pl (logique propositionnelle). Les logiques avancees (Description Logic, Modale, QBF - Tweety-3-Advanced-Logics) requierent d’autres clusters Tweety (dl, ml) non inclus dans cette DLL ; les notebooks Python restent canoniques pour ces logiques, ainsi que pour l’argumentation (Dung, notebooks 5-7) et les reseaux logiques markoviens (notebook 10).

Exercices

Adaptez ceux du notebook Python a l’API C# (cast PlFormula, méthodes Java minuscules). Rappel : les stubs doivent s’executer sans erreur (jamais raise/assert/1/0).

Le protocole des exercices. Les trois exercices rejouent les gestes des sections 2-4 en montant en généralité : le premier classifie une formule (tautologie / contradiction / contingence) — c’est une propriété absolue, indépendante de toute base ; le deuxième définit l’équivalence logique comme double entailment (F |= G et G |= F) — un cas particulier de la section 4 ; le troisième cherche une conséquence cachée d’une KB, là où l’intuition seule ne suffit plus. Les squelettes sont exécutables tels quels (C.1) ; pour chacun, la stratégie gagnante est la même qu’en cours : traduire la question en une requête sur les mondes, puis laisser l’énumérateur ou le SatReasoner trancher.

Exercice 1 : Tautologie, contradiction ou contingence ?

Ecrivez une fonction qui, etant donne une formule et une signature, determine si elle est tautologie (tous les mondes la satisfont), contradiction (aucun), ou contingente. Testez sur a || !a, a && !a, et a => b.

Indice : enumerer les mondes via PossibleWorldIterator, compter ceux qui satisfont la formule, comparer au total 2^n.

using org.tweetyproject.logics.pl.syntax;
using org.tweetyproject.logics.pl.semantics;
using org.tweetyproject.logics.pl.parser;

// TODO etudiant : implementer Classify(p, sig, formulaStr) -> "tautologie"/"contradiction"/"contingente"
string Classify(PlParser p, PlSignature sig, string formulaStr)
{
    var f = (PlFormula) p.parseFormula(formulaStr);
    int total = 0, satisfied = 0;
    // TODO : parcourir PossibleWorldIterator(sig), compter total et les mondes qui satisfont f
    return "Exercice 1 a completer";
}

var p = new PlParser();
var sig = new PlSignature();
sig.add(p.parseFormula("a"));
sig.add(p.parseFormula("b"));
Console.WriteLine(Classify(p, sig, "a || !a"));   // attendu : tautologie
Console.WriteLine(Classify(p, sig, "a && !a"));   // attendu : contradiction
Console.WriteLine(Classify(p, sig, "a => b"));    // attendu : contingente
Exercice 1 a completer
Exercice 1 a completer
Exercice 1 a completer

Exercice 2 : Equivalence logique via l’entaînement

Deux formules f1 et f2 sont logiquement equivalentes ssi f1 |= f2 ET f2 |= f1. Verifiez que a => b est equivalent a !a || b, et que !(a && b) est equivalent a !a || !b (loi de De Morgan).

Indice : construire un PlBeliefSet contenant f1, puis SatReasoner.query(kb, f2) ; recommencer en inversant. Equivalent ssi les deux sens sont vrais.

using org.tweetyproject.logics.pl.syntax;
using org.tweetyproject.logics.pl.reasoner;
using org.tweetyproject.logics.pl.parser;

// TODO etudiant : implementer AreEquivalent(p, f1Str, f2Str) -> bool
bool AreEquivalent(PlParser p, string f1Str, string f2Str)
{
    var f1 = (PlFormula) p.parseFormula(f1Str);
    var f2 = (PlFormula) p.parseFormula(f2Str);
    var r = new SatReasoner();
    // TODO : KB{f1} |= f2  ET  KB{f2} |= f1
    return false;  // TODO etudiant
}

var p = new PlParser();
Console.WriteLine(AreEquivalent(p, "a => b", "!a || b"));        // attendu : True
Console.WriteLine(AreEquivalent(p, "!(a && b)", "!a || !b"));    // attendu : True (De Morgan)
Console.WriteLine(AreEquivalent(p, "a => b", "b => a"));         // attendu : False
False
False
False

Exercice 3 : Deduire une consequence cachee

Soit la base KB = { (a || b) => c, c => d, a }. Quelles propositions parmi {a, b, c, d, e} sont entaînees par KB ? Utilisez SatReasoner.query pour tester chaque proposition et afficher celles qui sont consequences. Reflechissez ensuite : pourquoi d est-il entaîne alors qu’il n’apparait dans aucune premisse contenant directement a ?

Indice : a vrai + (a||b)=>c donne c vrai, puis c=>d donne d vrai. C’est le chainage avant des implications - verifiez-le machinelement.

using org.tweetyproject.logics.pl.syntax;
using org.tweetyproject.logics.pl.reasoner;
using org.tweetyproject.logics.pl.parser;

var p = new PlParser();
var kb = new PlBeliefSet();
kb.add(p.parseFormula("(a || b) => c"));
kb.add(p.parseFormula("c => d"));
kb.add(p.parseFormula("a"));

var r = new SatReasoner();
foreach (var atom in new[]{ "a", "b", "c", "d", "e" })
{
    // TODO etudiant : tester r.query(kb, atom) et afficher "KB |= atom : oui/non"
    Console.WriteLine($"KB |= {atom} ? (Exercice 3 a completer)");
}
KB |= a ? (Exercice 3 a completer)
KB |= b ? (Exercice 3 a completer)
KB |= c ? (Exercice 3 a completer)
KB |= d ? (Exercice 3 a completer)
KB |= e ? (Exercice 3 a completer)
Retour au sommet