Tweety C# / IKVM - Revision de Croyances (Port .NET du notebook Python)

Ce notebook porte en C# / .NET (via IKVM, sans JVM) le module belief-revision de TweetyProject. Il fait partie de l’Epic #4667 (portage .NET de la serie Tweety) et prolonge les notebooks déjà portes : logiques de base, sémantique, FOL, argumentation de Dung et ASPIC+.

Le pendant Python est Tweety-4-Belief-Revision.ipynb.

De quoi parle la revision de croyances ?

Un agent rationnel doit parfois integrer une information qui contredit ce qu’il croit déjà. Ajouter naivement la nouvelle formule a sa base la rendrait incoherente (elle impliquerait tout et n’importe quoi). La théorie AGM (Alchourron, Gardenfors, Makinson, 1985) formalise les trois opérations du changement de croyance :

  • Expansion (K + phi) : on ajoute phi sans se soucier de la coherence.
  • Contraction (K - phi) : on retire juste assez de croyances pour que K n’implique plus phi.
  • Revision (K * phi) : on integre phi en preservant la coherence, quitte a abandonner d’anciennes croyances.

L’identite de Levi relie les trois : K * phi = (K - !phi) + phi. On contracte d’abord par la negation de l’information, puis on expanse. Tweety implemente ces opérateurs ; ce notebook les execute reellement sur des bases propositionnelles.

Comment Tweety tourne en .NET (sans JVM)

Tweety est une bibliotheque Java. On la recompile en assembly .NET avec IKVM 8.15.0 : le bytecode Java devient du code .NET, appelable directement en C# depuis le kernel .net-csharp. La recette de build (Maven shade + <IkvmReference>) est documentee dans dotnet-build/.

1. Configuration du runtime IKVM

IKVM est un runtime Java sur .NET : il réimplémente la JVM et les bibliothèques de classes Java en bytecode .NET, ce qui permet de consommer un JAR Java (ici Tweety) sans installer de JVM — les types Java (java.util.HashSet, etc.) deviennent des types .NET utilisables directement depuis C#. La configuration référence deux paquets NuGet : le noyau IKVM et l’image de base IKVM.Image (les classes Java standard). IKVM.Image tire à son tour le runtime natif de chaque plateforme (IKVM.Image.runtime.<rid>, par exemple win-x64 ou linux-x64), et la cellule suivante choisit celui de la machine courante. La cellule suivante vérifie l’installation en reconstruisant le home d’IKVM — le témoin décisif étant le chargement de la base tzdb (fuseaux horaires Java) : si elle vaut True, le runtime est complet et fonctionnel.

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

Lecture du setup IKVM — la sortie IKVM 8.15.0 pret (home=ikvm-home-8.15.0-<rid>, tzdb=True) valide les trois étages du runtime : la version (8.15.0, alignée sur les directives #r de la cellule précédente), le home (le répertoire où IKVM dépose ses données — isolé par version et par plateforme, par exemple win-x64 sous Windows ou linux-x64 sous Linux), et surtout tzdb=True : la base des fuseaux horaires Java (timezone database) a été chargée. C’est le témoin le plus fin de la santé du runtime : tzdb n’est pas une dépendance de Tweety, c’est une composante profonde de l’image Java — si elle charge, l’émulation JVM est complète, pas seulement démarrée. Sans ce témoin, un #r silencieux peut laisser croire à un environnement prêt qui ne l’est pas.

2. Chargement de la DLL Tweety beliefdynamics

Tweety n’est pas publié sur NuGet en version .NET : l’équipe fournit des JAR Java. Le dépôt génère donc des DLL .NET via IKVM (une par module Tweety), stockées localement et chargées par directive #r. C’est la même mécanique que pour les notebooks Tweety déjà portés (logiques de base, sémantique, FOL, argumentation) — la DLL tweety-beliefdynamics apporte les opérateurs AGM : contraction par noyaux, expansion, révision par identité de Levi.

#r "org.tweetyproject.tweety-beliefdynamics.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-beliefdynamics.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-beliefdynamics v1.30.0.0 (9.0 Mo).

Lecture du chargement de la DLL — la sortie Tweety (IKVM) reference chargee : org.tweetyproject.tweety-beliefdynamics v1.30.0.0 (9,0 Mo) fait deux vérifications en une. D’abord l’existence et la lisibilité : AssemblyName.GetAssemblyName lit les métadonnées du fichier sans l’exécuter — si la DLL était absente ou corrompue, l’appel lèverait avant d’afficher quoi que ce soit. Ensuite l’identité : version 1.30.0.0 et taille 9,0 Mo — autant de points de contrôle pour diagnostiquer un conflit de version entre notebooks. Pourquoi cette vérification explicite ? Parce qu’en .NET Interactive, la directive #r est silencieuse par défaut (constat #5039, documenté dans les notebooks Tweety précédents) : elle n’échoue pas bruyamment si la référence est mauvaise — l’erreur n’apparaît que plus loin, au premier appel d’un type manquant, loin de sa cause. Vérifier tôt, c’est localiser l’erreur là où elle naît.

3. Le problème : une base de croyances incohérente

Le scénario fondateur de la révision : une base K cohérente (elle a des modèles), puis une nouvelle information !b qui contredit ce que K implique déjà (b). L’union naïve K + !b est incohérente — et une base incohérente, en logique classique, implique tout (principe d’explosion) : elle ne peut plus rien raisonner du tout. Le test de cohérence se fait sans solveur SAT externe : SimplePlReasoner énumère les interprétations et vérifie si la base possède au moins un modèle. Trois questions structurent la sortie : K est-elle incohérente ? l’union naïve l’est-elle ? — et la section suivante montrera l’opérateur qui intègre !b sans produire cette explosion.

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

var parser = new PlParser();
var reasoner = new SimplePlReasoner();

// Test de coherence sans solveur SAT externe : une base est INCOHERENTE si et seulement
// si elle entraine une contradiction (elle n'a alors aucun modele). On reutilise donc le
// raisonneur propositionnel : query(base, "a && !a") vaut true ssi la base est incoherente.
var faux = (PlFormula) parser.parseFormula("a && !a");

// Base de croyances initiale  K = { a, a=>b, !c }  (coherente).
var K = new PlBeliefSet();
K.add((PlFormula) parser.parseFormula("a"));
K.add((PlFormula) parser.parseFormula("a=>b"));
K.add((PlFormula) parser.parseFormula("!c"));
Console.WriteLine($"Base initiale         K = {K}");
Console.WriteLine($"K incoherente ?           {reasoner.query(K, faux)}");

// Nouvelle information  phi = !b. Or a et a=>b impliquent b : phi contredit K.
// L'union naive  K + [ !b ]  est donc incoherente.
var naive = new PlBeliefSet();
naive.add((PlFormula) parser.parseFormula("a"));
naive.add((PlFormula) parser.parseFormula("a=>b"));
naive.add((PlFormula) parser.parseFormula("!c"));
naive.add((PlFormula) parser.parseFormula("!b"));
Console.WriteLine($"Union naive K + [!b]  = {naive}");
Console.WriteLine($"Union naive incoherente ? {reasoner.query(naive, faux)}");
Base initiale         K = { (a=>b), a, !c }
K incoherente ?           false
Union naive K + [!b]  = { (a=>b), a, !b, !c }
Union naive incoherente ? true

Interpretation

La sortie donne la diagonale du problème : K incoherente ? false, puis Union naive incoherente ? true. La base initiale K = { (a=>b), a, !c } a des modèles (par exemple a=1, b=1, c=0), elle raisonne sainement. L’union naïve { (a=>b), a, !b, !c } n’en a plus : a et a=>b forcent b, que !b nie — contradiction, donc zéro modèle, donc l’entraînement de n’importe quelle formule (principe d’explosion). C’est le mur que la révision AGM va contourner : intégrer !b en abandonnant juste ce qu’il faut des anciennes croyances, plutôt que de tout faire exploser. La suite du notebook montre les deux opérateurs qui réalisent ce compromis — contraction puis révision.

4. Contraction par noyaux (kernel contraction)

La théorie des noyaux (Hansson) définit la contraction élégamment : un noyau pour b est un sous-ensemble minimal de K qui implique b — enlever n’importe laquelle de ses formules suffit à briser l’entraînement de b. Pour que K n’implique plus b, il faut couper au moins une formule dans chaque noyau : c’est le rôle de la fonction d’incision (incision function). Tweety assemble le tout : KernelContractionOperator prend le fournisseur de noyaux (SimplePlReasoner) et la fonction d’incision — ici RandomIncisionFunction, qui choisit arbitrairement. La sortie vérifie la propriété garantie (ne plus impliquer b) et montre la base résultante — dont le contenu exact dépend du choix (aléatoire) de l’incision.

using java.util;
using org.tweetyproject.logics.pl.reasoner;
using org.tweetyproject.beliefdynamics.kernels;

// La contraction retire juste ce qu'il faut pour que la base n'implique plus b.
// KernelContractionOperator(fonction d'incision, fournisseur de noyaux).
//   - SimplePlReasoner joue le role de KernelProvider (il enumere les noyaux).
//   - RandomIncisionFunction choisit dans chaque noyau la formule a couper.
var baseK = new HashSet();
baseK.add((PlFormula) parser.parseFormula("a"));
baseK.add((PlFormula) parser.parseFormula("a=>b"));
baseK.add((PlFormula) parser.parseFormula("!c"));

var aRetirer = new HashSet();
aRetirer.add((PlFormula) parser.parseFormula("b"));

var contraction = new KernelContractionOperator(new RandomIncisionFunction(), new SimplePlReasoner());
var contractee = contraction.contract(baseK, aRetirer);
Console.WriteLine($"K contractee par b = {contractee}");

// La base contractee ne doit plus entrainer b. On reconstruit une PlBeliefSet a partir
// de la collection retournee, puis on interroge le raisonneur.
var contracteeKb = new PlBeliefSet();
var itc = contractee.iterator();
while (itc.hasNext()) contracteeKb.add((PlFormula) itc.next());
var b = (PlFormula) parser.parseFormula("b");
Console.WriteLine($"Entraine encore b ? {reasoner.query(contracteeKb, b)}");
K contractee par b = [a, !c]
Entraine encore b ? false

Interpretation

La sortie lit : K contractee par b = [a, !c], puis Entraine encore b ? false. Autrement dit, c’est la formule (a=>b) qui a été sacrifiée — la base finale {a, !c} ne contient plus le seul chemin vers b. La lecture théorique : le noyau pour b était {a, (a=>b)} (minimal : retirer soit a, soit a=>b brise l’entraînement), et l’incision aléatoire a choisi (a=>b). Ce qui est garanti, ce qui ne l’est pas : la propriété « ne plus impliquer b » est garantie quel que soit le choix ; la formule exactement retirée, elle, varie d’une exécution à l’autre sous RandomIncisionFunction. Une incision informée (préférences épistémiques — « je tiens plus à mes faits qu’à mes règles ») produirait un choix déterministe et justifiable : c’est précisément l’axe de conception que l’exemple pingouin de la section 6 rendra visible.

5. Révision par l’identité de Levi

La révision K * phi intègre phi en préservant la cohérence. L’identité de Levi la réduit à deux opérations déjà connues : K * phi = (K - !phi) + phi — contracter par la négation de la nouvelle information (retirer ce qui contredirait phi), puis expanser par phi elle-même. Tweety l’implémente littéralement : LeviMultipleBaseRevisionOperator compose la contraction de la section 4 avec DefaultMultipleBaseExpansionOperator. La sortie vérifie les trois propriétés attendues du résultat : cohérent, contient bien la nouvelle information, et — c’est visible dans son contenu — cohérent avec la base contractée de la section précédente.

using org.tweetyproject.beliefdynamics;

// Identite de Levi :  K * phi  =  (K - !phi) + phi
//   revision = contraction par la negation de l'information, puis expansion.
var expansion = new DefaultMultipleBaseExpansionOperator();
var levi = new LeviMultipleBaseRevisionOperator(contraction, expansion);

var nouvelleInfo = new HashSet();
nouvelleInfo.add((PlFormula) parser.parseFormula("!b"));

var revisee = levi.revise(baseK, nouvelleInfo);
Console.WriteLine($"K revisee par !b (Levi) = {revisee}");

var reviseeKb = new PlBeliefSet();
var itr = revisee.iterator();
while (itr.hasNext()) reviseeKb.add((PlFormula) itr.next());
var notB = (PlFormula) parser.parseFormula("!b");
Console.WriteLine($"Resultat incoherent ?     {reasoner.query(reviseeKb, faux)}");
Console.WriteLine($"Contient bien !b ?        {reviseeKb.contains(notB)}");
K revisee par !b (Levi) = [a, !b, !c]
Resultat incoherent ?     false
Contient bien !b ?        True

Interpretation

La sortie : K revisee par !b (Levi) = [a, !b, !c], Resultat incoherent ? false, Contient bien !b ? True. La lecture fine : le résultat est exactement la base contractée de la section 4 ([a, !c] — où l’incision avait retiré (a=>b)) à laquelle l’expansion a ajouté !b. L’identité de Levi est visible dans le contenu de la sortie, pas seulement dans la formule : réviser par !b = contracter par b (section 4) puis ajouter !b. Et le contraste avec la section 3 est total : l’union naïve {(a=>b), a, !b, !c} était incohérente ; la révision {a, !b, !c} intègre la même information en restant raisonnable — au prix d’une croyance abandonnée (a=>b). C’est le compromis AGM : toute nouvelle information s’installe, le minimum de l’ancien se sacrifie.

6. Exemple guide : le pingouin Tweety (raisonnement non-monotone)

La bibliotheque tire son nom de Tweety, l’oiseau emblematique du raisonnement non-monotone. Partons de trois croyances : Tweety est un pingouin (p), un pingouin est un oiseau (p => b), un oiseau vole (b => f). La base conclut donc que Tweety vole. Puis on observe que ce pingouin ne vole pas (!f). Pour integrer l’observation, la revision doit abandonner une règle par defaut de la chaîne de raisonnement p => b => f. C’est un problème non-trivial : l’incoherence est derivee (via une chaîne d’implications), pas directe.

Le notebook affiche la ou les croyances effectivement sacrifiees. Notez qu’une contraction AGM n’est pas unique : plusieurs retraits minimaux restaurent la coherence (ici retirer p => b ou b => f). Le choix depend de la fonction d’incision (RandomIncisionFunction) ; un opérateur muni de priorites sur les croyances retirerait preferentiellement la règle la moins fiable.

// Exemple guide : le pingouin Tweety (raisonnement non-monotone).
// p = "est un pingouin", b = "est un oiseau", f = "vole".
// K = { p, p=>b, b=>f }  =>  la base conclut que Tweety vole.
var Kt = new HashSet();
Kt.add((PlFormula) parser.parseFormula("p"));
Kt.add((PlFormula) parser.parseFormula("p=>b"));
Kt.add((PlFormula) parser.parseFormula("b=>f"));

var KtKb = new PlBeliefSet();
var itk = Kt.iterator();
while (itk.hasNext()) KtKb.add((PlFormula) itk.next());
var f = (PlFormula) parser.parseFormula("f");
Console.WriteLine($"K conclut que Tweety vole (f) ? {reasoner.query(KtKb, f)}");

// Observation : ce pingouin ne vole PAS. On revise K par !f.
var obs = new HashSet();
obs.add((PlFormula) parser.parseFormula("!f"));
var reviseeTweety = levi.revise(Kt, obs);
Console.WriteLine($"K revisee par !f = {reviseeTweety}");

var rtKb = new PlBeliefSet();
var itt = reviseeTweety.iterator();
while (itt.hasNext()) rtKb.add((PlFormula) itt.next());
var notF = (PlFormula) parser.parseFormula("!f");
Console.WriteLine($"Resultat incoherent ?         {reasoner.query(rtKb, faux)}");
Console.WriteLine($"Conclut desormais !f (ne vole pas) ? {rtKb.contains(notF)}");

// Quelle(s) croyance(s) la revision a-t-elle du sacrifier ?
var abandonnees = new java.util.ArrayList();
var itd = Kt.iterator();
while (itd.hasNext()) {
    var croyance = (PlFormula) itd.next();
    if (!reviseeTweety.contains(croyance)) abandonnees.add(croyance);
}
Console.WriteLine($"Croyance(s) abandonnee(s) par la revision : {abandonnees}");
Console.WriteLine();
Console.WriteLine("La revision a du abandonner une regle par defaut de la chaine p=>b=>f pour");
Console.WriteLine("integrer l'observation !f sans contradiction : c'est le coeur de l'AGM.");
K conclut que Tweety vole (f) ? true
K revisee par !f = [(b=>f), p, !f]
Resultat incoherent ?         false
Conclut desormais !f (ne vole pas) ? True
Croyance(s) abandonnee(s) par la revision : [(p=>b)]

La revision a du abandonner une regle par defaut de la chaine p=>b=>f pour
integrer l'observation !f sans contradiction : c'est le coeur de l'AGM.

Lecture de la révision du pingouin — la sortie raconte l’intégralité du compromis AGM en cinq lignes : K conclut que Tweety vole (f) ? true (la base initiale raisonne sainement — c’est sa conclusion qui est fausse, pas sa logique), puis après révision par !f : K revisee = [(b=>f), p, !f], cohérente, concluant désormais !f. Et la ligne clé : Croyance(s) abandonnee(s) : [(p=>b)].

Ce que l’abandon révèle : pour intégrer « ce pingouin ne vole pas », il faut couper la chaîne p => b => f quelque part — deux incisions minimales existent : retirer p=>b (« les pingouins ne sont pas des oiseaux ») ou retirer b=>f (« les oiseaux ne volent pas forcément »). L’intuition biologique dit clairement : sacrifie b=>f, garde p=>b. Mais RandomIncisionFunction n’a aucune préférence épistémique — elle a tiré p=>b, produisant une révision valide mais absurde (un pingouin qui ne serait pas un oiseau). La leçon de conception : la théorie AGM garantit la cohérence du résultat, jamais sa pertinence — la fonction d’incision est le point d’injection des connaissances de domaine. C’est exactement ce que la sortie affirme en conclusion : « abandonner une règle par défaut… c’est le cœur de l’AGM » — le cœur, et la responsabilité.

Conclusion

Ce notebook a exécuté, en C# natif via IKVM, les opérateurs AGM de Tweety :

  • test de cohérence par existence de modèle (SimplePlReasoner) : une base est incohérente ssi elle n’a aucun modèle — l’union naïve {(a=>b), a, !b, !c} l’a démontré ;
  • contraction par noyaux (KernelContractionOperator + RandomIncisionFunction) : retirer (a=>b) suffit à ne plus impliquer b — propriété garantie, choix d’incision aléatoire ;
  • révision par l’identité de Levi (LeviMultipleBaseRevisionOperator) : le résultat [a, !b, !c] est littéralement la base contractée + la nouvelle formule ;
  • une application non-monotone (le pingouin Tweety) où la révision résout une incohérence dérivée — via une chaîne d’implications, pas une contradiction directe — en abandonnant une règle de la chaîne p => b => f.

Trois idées à retenir au-delà des opérateurs : (1) une base incohérente ne « dégrade » pas le raisonnement, elle l’annule (explosion) — la cohérence n’est pas une option ; (2) le changement de croyance minimal n’est jamais unique — la fonction d’incision encode les préférences épistémiques de l’agent ; (3) l’identité de Levi fait de la révision une composition : bien la comprendre, c’est pouvoir l’auditer cellule par cellule, comme ce notebook l’a fait. La révision de croyances est au cœur des systèmes qui apprennent en présence d’informations contradictoires : mise à jour de bases de connaissances, fusion de sources, diagnostic. Le notebook Python compagnon poursuit avec les mesures d’incohérence et l’énumération de MUS (sous-ensembles incohérents minimaux).

Exercices

Les exercices ci-dessous réutilisent les opérateurs construits plus haut (levi, la contraction par noyaux, le raisonneur reasoner, le parser). Complétez les stubs ; la base reste exécutable de bout en bout même si les exercices ne sont pas remplis.

Critères de réussite (vérifiables sur la sortie de chaque exercice) :

  • Exercice 1 (réviser K = {pluie, pluie => sol_mouille} par !sol_mouille) : la base révisée doit être cohérente (incoherent ? false) et contenir !sol_mouille — l’une des deux formules initiales aura été sacrifiée par l’incision (laquelle ? ça dépend du tirage).
  • Exercice 2 (contracter K = {x, x=>y, y=>z} par z) : après contraction, la base ne doit plus impliquer z — en général deux noyaux existent ({x, x=>y}… la chaîne complète), et l’incision doit couper chaque chemin vers z.
  • Exercice 3 (révision vs union naïve sur K = {m, m=>n, !o} et !n) : l’union naïve compte 4 formules et est incohérente ; la base révisée compte au plus 4 formules (au moins une sacrifiée) et reste cohérente — l’écart de cardinal entre les deux mesure le coût épistémique de la cohérence.
// Exercice 1 : reviser votre propre base de croyances.
// Objectif : construire K = { pluie, pluie => sol_mouille } puis reviser par !sol_mouille.
// Indice : reutilisez le patron levi.revise(base, nouvelleInfo) et testez la coherence.
// Etape 1 : construire la HashSet baseEx1 avec les deux formules.
// Etape 2 : construire nouvelleInfoEx1 = { !sol_mouille }.
// Etape 3 : appeler levi.revise(...) et afficher le resultat + sa coherence.

// var baseEx1 = new HashSet();
// TODO : completer
Console.WriteLine("Exercice 1 a completer");
Exercice 1 a completer
// Exercice 2 : contraction par noyaux.
// Objectif : partir de K = { x, x=>y, y=>z } et la contracter par z.
// Indice : new KernelContractionOperator(new RandomIncisionFunction(), new SimplePlReasoner()).
// Etape 1 : construire la base et l'ensemble { z } a retirer.
// Etape 2 : appeler .contract(base, aRetirer).
// Etape 3 : verifier avec un SimplePlReasoner que la base contractee n'implique plus z.

// TODO : completer
Console.WriteLine("Exercice 2 a completer");
Exercice 2 a completer
// Exercice 3 : revision vs union naive (mesure de l'ecart).
// Objectif : sur K = { m, m=>n, !o }, comparer |K + {!n}| (union naive, incoherente)
//            au cardinal de la base revisee levi.revise(K, {!n}) (coherente).
// Indice : la revision retire au moins une formule ; comptez .size() de chaque cote.
// Etape 1 : construire K et la nouvelle information { !n }.
// Etape 2 : calculer l'union naive et la base revisee.
// Etape 3 : afficher les deux cardinaux et la difference (nombre de croyances sacrifiees).

// TODO : completer
Console.WriteLine("Exercice 3 a completer");
Exercice 3 a completer
Retour au sommet