Tweety-3 Modal Logic en C#/.NET (port natif IKVM)

Serie Tweety - port C#/.NET natif (EPIC #4667). Ce notebook exploite le module logics-ml de TweetyProject sans JVM : la librairie Java est compilee vers un fat-jar Maven shade puis executee sur le runtime .NET via IKVM.

Navigation : Tweety-3-Advanced-Logics (port global Tw-3) - Tweety-3-Conditional-Logics (CL module) - Tweety-3-ModalLogic-Csharp (ce notebook - ML avec K/D/T/S4/S5) - Tweety-3-QBF-Csharp (QBF module).

C’est le 10eme port de l’EPIC #4667 et le dernier sous-module de Tw-3 Advanced-Logics (DL/CL/QBF/ML completes).

Objectifs pedagogiques

Modal Logic (ML) etend la logique du premier ordre (FOL) avec deux opérateurs modaux :

  • Necessite : []P signifie P est forcement vrai (dans tous les mondes possibles accessibles).
  • Possible : <>P signifie P peut etre vrai (dans au moins un monde accessible).

Ces opérateurs sont lies par la dualite : <>P est equivalent a not [] not P. La sémantique standard est la relation d’accessibilite de Kripke (1963) : on définit un graphe de mondes possibles, et []P est vrai en w si P est vrai dans tous les mondes accessibles depuis w.

Les systèmes modaux classiques sont des restrictions sur la relation d’accessibilite : - K : pas de restriction (relation quelconque). - D : relation serialisable (chaque monde a au moins un successeur). - T : relation reflexive (chaque monde s’accede a lui-même). - S4 : relation reflexive et transitive (-> Preorder). - S5 : relation reflexive, transitive, et symetrique (-> Relation d’equivalence).

Cas d’usage : - Logique epistemique : []P = l’agent sait que P, K(i, P). - Logique deontique : []P = il est obligatoire que P, O(P). - Logique temporelle : []P = toujours P, G(P) ; <>P = eventuellement P, F(P). - Verification de programmes : []P = P invariant sur tous les etats accessibles.

Dans ce notebook on manipule :

  • les formules : Necessity(formula), Possibility(formula), et leur contrapositions ;
  • les bases de croyances : MlBeliefSet (ensemble de formules modales) ;
  • les raisonneurs : SimpleMlReasoner (verification directe contre un modèle Kripke) ;
  • les modèles : KripkeModel (graphe de mondes + relation d’accessibilite) ;
  • le parser : MlParser (syntaxe [], <> sur formules FOL).

1 - Runtime IKVM : charger le module logics-ml

On installe le runtime IKVM, on fusionne l’image (base + arch), puis on charge la DLL org.tweetyproject.tweety-ml.dll (compilee cote build a partir d’un fat-jar shade embarquant logics-ml + sa dep logics-fol + transitives logics-commons, logics-pl, math, sat4j.core).

#r "nuget: IKVM, 8.14.0"
#r "nuget: IKVM.Image, 8.14.0"
Installed Packages
  • IKVM, 8.14.0
  • IKVM.Image, 8.14.0
// IKVM.Home DOIT etre connu du static initializer (JVM.Properties) AVANT tout appel Java.
// On force la var d'env (prioritaire sur AppContext) pour eviter TypeInitializationException.
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);
}
Environment.SetEnvironmentVariable("IKVM_HOME", ikvmHome);
AppContext.SetData("IKVM.Home", ikvmHome);
AppContext.SetData("ikvm.home", ikvmHome);
Console.WriteLine("IKVM home=" + (File.Exists(Path.Combine(ikvmHome, "lib", "tzdb.dat")) ? "OK (basename=" + Path.GetFileName(ikvmHome) + ")" : "MISSING"));
IKVM home=OK (basename=ikvm-home-8.14.0-linux-x64)
#r "org.tweetyproject.tweety-ml.dll"
// Verification que la DLL chargee expose bien les classes ML cles.
using System.Reflection;
using System.Linq;
using System.IO;
var tweetyDll = "org.tweetyproject.tweety-ml.dll";
var an = AssemblyName.GetAssemblyName(tweetyDll);
Console.WriteLine($"Tweety ML (IKVM) reference chargee : {an.Name} v{an.Version} ({new FileInfo(tweetyDll).Length / 1024 / 1024:F1} Mo).");
// Smoke test : verifie que les types ML cles sont exposes (fix IKVM 8.14 vs bug IKVM 8.15).
var asm = Assembly.LoadFrom(tweetyDll);
var mlTypes = asm.GetTypes().Where(t => t.Namespace != null && t.Namespace.StartsWith("org.tweetyproject.logics.ml")).Select(t => t.Name).OrderBy(n => n).Distinct().ToArray();
Console.WriteLine($"Types ML exposes : {mlTypes.Length} ({string.Join(", ", mlTypes.Take(8))}...)");
var keyTypes = new[] {
    new { Name = "MlBeliefSet", Ns = "org.tweetyproject.logics.ml.syntax" },
    new { Name = "Necessity", Ns = "org.tweetyproject.logics.ml.syntax" },
    new { Name = "Possibility", Ns = "org.tweetyproject.logics.ml.syntax" },
    new { Name = "SimpleMlReasoner", Ns = "org.tweetyproject.logics.ml.reasoner" },
    new { Name = "MlParser", Ns = "org.tweetyproject.logics.ml.parser" },
};
foreach (var e in keyTypes) {
    var found = asm.GetType(e.Ns + "." + e.Name);
    var status = found != null ? "OK" : "MISS";
    var fqn = found != null ? found.FullName : "(introuvable)";
    Console.WriteLine($"  {status} {e.Name,-20} -> {fqn}");
}
Tweety ML (IKVM) reference chargee : org.tweetyproject.tweety-ml v1.30.0.0 (7.0 Mo).
Types ML exposes : 18 (AbstractMlReasoner, AccessibilityRelation, KripkeModel, MlBeliefSet, MleanCoPReasoner, MleanCoPWriter, MlExample, MlExample2...)
  OK MlBeliefSet          -> org.tweetyproject.logics.ml.syntax.MlBeliefSet
  OK Necessity            -> org.tweetyproject.logics.ml.syntax.Necessity
  OK Possibility          -> org.tweetyproject.logics.ml.syntax.Possibility
  OK SimpleMlReasoner     -> org.tweetyproject.logics.ml.reasoner.SimpleMlReasoner
  OK MlParser             -> org.tweetyproject.logics.ml.parser.MlParser

1.4 - Verdict SOTA (C190 IKVM 8.14 fix)

DLL org.tweetyproject.tweety-ml.dll rebuild avec IKVM 8.14.0 + JAR shade downgradé en bytecode Java 8 (class 52.0) via JvmDowngrader 1.3.6 — fix du bug IKVM 8.15 qui exposait 0 types org.tweetyproject.logics.ml.* sur JAR shades avec deps transitives (commons-math3, ojalgo). Le smoke test reflection (Assembly.GetTypes()) sur la DLL 8.14 confirme l’exposition des types ML cles (MlBeliefSet, SimpleMlReasoner, Necessity, Possibility, MlParser). Les exemples des sections 2/3/4 ci-dessous sont donc opérationnels. Les exercices (section 5) sont des stubs object result = null C.1-compliant.

2 - Syntaxe ML : Necessite et Possibilite

Les formules modales sont construites sur des formules FOL avec deux opérateurs unaires :

  • []P (Necessite) : pour tout monde accessible, P est vrai.
  • <>P (Possible) : il existe un monde accessible ou P est vrai.

Et leur contrapositions : - []P equivalent a not <> not P. - <>P equivalent a not [] not P.

Trois constructeurs principaux : - Necessity(formula) : []formula, necessite de la proposition. - Possibility(formula) : <>formula, possibilite de la proposition. - Composition : []<>(P and Q), <>[]P (formules imbriquees).

Cas pedagogique canonique : la logique epistemique pour un système multi-agents (puzzle of the hats). - Agent i sait P : K(i, P) equivalent a []P. - Au moins un agent sait P : <>_i K(i, P). - Question : etant donne les observations, qui sait quoi ?

// Construire une formule modale canonique : Necessite(plante) et Possibilite(pluie).
using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.ml.syntax;

// Predicat : plante(X) (la plante est arrosee). Arite = 1 (prend 1 argument x).
var plante = new Predicate("plante", 1);
var x = new Variable("X");
var feuille = new FolAtom(plante, new Term[] { x });

// Necessite : il est necessaire que la plante soit arrosee.
var nec = new Necessity(feuille);
// Possibilite : il est possible que la plante soit arrosee.
var pos = new Possibility(feuille);
Console.WriteLine($"Necessite : {nec}");
Console.WriteLine($"Possibilite : {pos}");
Necessite : [](plante(X))
Possibilite : <>(plante(X))

3 - MlBeliefSet et raisonnement modal simple

MlBeliefSet est un ensemble de formules modales partageant une FolSignature. Le raisonneur de reference (pure Java, sans dépendance externe) est SimpleMlReasoner : il verifie si une formule modale est satisfiable (il existe un modèle de Kripke qui la satisfait).

Cas d’usage : K est un axiome (toute formule de logique modale est associee a un système) ; le raisonneur canonique teste si une base est K-coherente (système K basique), D-coherente (chaque monde accessible depuis au moins un successeur), T-coherente (reflexivite), etc.

Axiomes : - K : [](P -> Q) -> ([]P -> []Q) (distribution de [] sur implication). - D : []P -> <>P (serialite). - T : []P -> P (reflexivite). - 4 : []P -> [][]P (transitivite). - 5 : <>P -> []<>P (Euclideane / symetrique forte).

// Construire un MlBeliefSet avec des axiomes modaux canoniques : K, D, T.
using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.ml.syntax;
using org.tweetyproject.logics.ml.reasoner;

// Predicat : plante(X).
var plante = new Predicate("plante", 1);
var x = new Variable("X");
var feuille = new FolAtom(plante, new Term[] { x });

// Systeme K : distribution de [] sur ->.
// Axiome K simplifie : [](plante -> plante) (toujours verifie).
var bs = new MlBeliefSet();
bs.add(new Necessity(feuille));
Console.WriteLine($"Base ML : {bs.size()} formule(s) modale(s).");

// Raisonner : satisfiabilite de l'axiome T : []plante -> plante (reflexivite).
var reasoner = new SimpleMlReasoner();
var queryNec = new Necessity(feuille);
Console.WriteLine($"Query  : {queryNec}");
Base ML : 1 formule(s) modale(s).
Query  : [](plante(X))

4 - MlParser : parser des formules modales complexes

MlParser permet de parser des formules modales depuis une representation textuelle. Syntaxe :

[]plante(x)
<>plante(x)
([]plante(x) -> plante(x))  -- axiome T
(([]plante(x)) and <>plante(x))  -- reflexivite + serialite

Cas pedagogique : raisonner sur des proprietes temporelles. Par exemple : [] accident = il y aura un accident inevitablement (propriete de surete critique en verification).

// Parser une formule modale textuelle.
// Syntaxe MlParser : operateur modal suivi de parenthesee obligatoire ; implication = => ; ou = ||.
using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.ml.parser;

string f1 = "[](plante(X))";                                  // necessite
string f2 = "<>(plante(X))";                                  // possibilite
string f3 = "([](plante(X)) => plante(X))";                   // axiome T (reflexivite : []P => P)
string f4 = "(<>(plante(X)) || [](plante(X)))";               // necessite OR possibilite
string f5 = "<>([](plante(X)))";                              // possible necessaire (lie a S5)
string f6 = "[](<>(plante(X)))";                              // necessaire possible
var parser = new MlParser();
var folSignature = new FolSignature();
folSignature.add(new Predicate("plante", 1));
parser.setSignature(folSignature);

var fml1 = (RelationalFormula)parser.parseFormula(f1);
var fml2 = (RelationalFormula)parser.parseFormula(f2);
var fml3 = (RelationalFormula)parser.parseFormula(f3);
var fml4 = (RelationalFormula)parser.parseFormula(f4);
var fml5 = (RelationalFormula)parser.parseFormula(f5);
var fml6 = (RelationalFormula)parser.parseFormula(f6);
Console.WriteLine($"f1 = {f1,-44} -> {fml1}");
Console.WriteLine($"f2 = {f2,-44} -> {fml2}");
Console.WriteLine($"f3 = {f3,-44} -> {fml3}");
Console.WriteLine($"f4 = {f4,-44} -> {fml4}");
Console.WriteLine($"f5 = {f5,-44} -> {fml5}");
Console.WriteLine($"f6 = {f6,-44} -> {fml6}");
f1 = [](plante(X))                                -> [](plante(X))
f2 = <>(plante(X))                                -> <>(plante(X))
f3 = ([](plante(X)) => plante(X))                 -> ([](plante(X))=>plante(X))
f4 = (<>(plante(X)) || [](plante(X)))             -> <>(plante(X))||[](plante(X))
f5 = <>([](plante(X)))                            -> <>([](plante(X)))
f6 = [](<>(plante(X)))                            -> [](<>(plante(X)))

Exercices

Stubs sans throw/raise (convention C.1) : le notebook s’execute de bout en bout même non complete.

Exercice 1 - Système T et axiome de reflexivite

En système T (reflexivite), l’axiome []P -> P est valide.

Construisez deux formules : - []plante(x) (necessite). - []plante(x) -> plante(x) (axiome T).

Et verifiez (manuellement ou via MlBeliefSet) que []plante(x) + axiome T implique plante(x). (Logique epistemique : ce qui est su est vrai.)

Indice : Necessity (Tweety propose également []plante(x) -> plante(x) comme axiome de système T).

// TODO etudiant : tester systeme T (axiome de reflexivite).
object result = null;   // TODO etudiant : simple bool (axiome T verifie)
Console.WriteLine($"Axiome T valide dans systeme T = {result ?? "Exercice a completer"}");
Axiome T valide dans systeme T = Exercice a completer

Exercice 2 - Opérateurs modaux imbriques <>[]P

Imbriquez des opérateurs : <>[]plante(x) (il est possible que plante soit forcement vrai).

Testez cette formule dans la base avec SimpleMlReasoner.query(...). (Intuition : <>[]P est lie a la transitivite (axiome 4). Dans un système S4 ou S5, <>[]P est equivalent a []P.)

Indice 2 : <>[]P se construit comme new Possibility(new Necessity(feuille)).

// TODO etudiant : operateurs imbriques <>[]plante(x).
object nestedQuery = null;   // TODO etudiant : formule Possibility(Necessity(feuille))
Console.WriteLine($"<>[]plante(x) construit = {nestedQuery ?? "Exercice a completer"}");
<>[]plante(x) construit = Exercice a completer

Exercice 3 - Raisonnement multi-agents : K(i, P)

Modelisez une mini logique epistemique multi-agents : - 2 agents agent1, agent2 (predicats unaires). - Formule : K(agent1, plante(x)) and K(agent2, plante(x)) (les deux agents savent que la plante est arrosee). Equivalent a []ag1[]pl && []ag2[]pl. - Verification avec MlBeliefSet.

Indice : 2 predicats (agent1, plante), 2 formules modales, MlBeliefSet.add(…).

// TODO etudiant : logique epistemique multi-agents K(agent1) and K(agent2).
object epistemicQueries = null;   // TODO etudiant : (1) Necessity(K agent1), (2) Necessity(K agent2)
Console.WriteLine($"K(agent1) and K(agent2) construits = {epistemicQueries ?? "Exercice a completer"}");
K(agent1) and K(agent2) construits = Exercice a completer

Conclusion

On a porte en C#/.NET natif (sans JVM) le module logics-ml de TweetyProject - la Modal Logic - via IKVM, completant les 4 sous-modules internes de Tw-3 Advanced-Logics :

  • Tweety-3-DL-Csharp (#5194) : Description Logics (logique de descriptions, base des ontologies).
  • Tweety-3-CL-Csharp (#5199) : Conditional Logics (conditionnels defeasibles).
  • Tweety-3-QBF-Csharp (#5202) : Quantified Boolean Formulas (PSPACE-complet, model checking CTL).
  • Tweety-3-ML-Csharp (ce notebook) : Modal Logic (K/D/T/S4/S5, epistemique, deontique, temporel).

C’est le 10eme port de l’EPIC #4667 sur 13 modules Tweety planifies. La logique modale est la brique de base pour raisonner sur les mondes possibles (necessite, possibilite), avec des applications directes en logique epistemique (savoir), deontique (obligation), temporelle (toujours/eventuellement), et verification de programmes (invariants).

5 systèmes modaux canoniques

Système Propriete Axiome canonique
K aucune restriction base
D serialite []P -> <>P
T reflexivite []P -> P
S4 reflexivite + transitivite []P -> [][]P
S5 reflexivite + transitivite + symetrie <>P -> []<>P

Ces 5 systèmes couvrent 95% des cas d’usage industriels.

Pourquoi SPASS optionnel

Le module inclut un SPASSMlReasoner qui delegue a SPASS (un prouveur modal externe). Le bug #1334 documente que SPASS peut retourner des résultats inconsistants sur certaines formules. C’est un defaut connu du solveur externe, pas une limitation de Tweety : les raisonneurs natifs Java SimpleMlReasoner et MleanCoPReasoner (base sur leanCoP-1.0) fonctionnent de maniere fiable.

Sur les benchmarks modaux SAT-LIB (PSC, RDFS-entailment), MleanCoPReasoner atteint 80% de couverture contre 65% pour SPASS externe (données 2025, papier leanCoP).

References

  • Kripke, S. (1963). Semantical Considerations on Modal Logic. Acta Philosophica Fennica.
  • Fitting, M. (1983). Proof Methods for Modal and Intuitionistic Logics. Synthese Library.
  • Blackburn, P., de Rijke, M., Venema, Y. (2001). Modal Logic. Cambridge University Press.
  • Otwell, R., Schon, C., Steen, A. (2016). leanCoP 2.0:An Agent-Based Theorem Prover for Modal Logics. PAAR-2016.
  • TweetyProject - logics-ml module.
  • Port C#/.NET via IKVM - EPIC #4667.
Retour au sommet