#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 — Description Logics en C#/.NET (port natif IKVM)
Serie Tweety — port C#/.NET natif (EPIC #4667). Ce notebook exploite le module
logics-dlde 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-2b-Semantics-Csharp (mondes possibles) · Tweety-2c-FOL-Csharp (premier ordre) · Tweety-3-Dung-Csharp (argumentation abstraite) · Tweety-3-Advanced-Logics (ce notebook — DL).
Objectifs pedagogiques
Les Description Logics (DL) sont le fragment decidable de la logique du premier ordre qui sous-tend les ontologies (web sémantique, OWL, bases de connaissances medicales ou industrielles). Elles equilibrent expressivite et decidabilite via une syntaxe compacte dediee aux concepts, rôles et individus.
Dans ce notebook on manipule :
- la TBox : ensemble d’axiomes terminologiques (definitions de concepts, inclusions) ;
- la ABox : ensemble d’assertions sur les individus (appartenance a un concept, relations de rôle) ;
- le reasoner
NaiveDlReasoner: un raisonneur naif (mais fonctionnel) qui repond aux requêtes de subsomption et d’instance ; - le parser
DlParser: analyse syntaxique des expressions DL classiques (AL, ALC, SHIQ simplifie).
L’objectif : faire valoir la specificite des DL face au propositionnel (Tweety-2) et a l’abstrait (Dung) — raisonner sur des hiérarchies de concepts plutot que sur des booléens ou des graphes d’attaque.
1 — Runtime IKVM : charger le module logics-dl
On installe le runtime IKVM, on fusionne l’image (base + arch), puis on charge la DLL org.tweetyproject.tweety-advanced-logics.dll (compilee cote build a partir d’un fat-jar shade embarquant logics-dl + ses dependances transitives : logics-commons, fol, pl, math, commons, sat4j, commons-math).
Note de parite cross-langage (EPIC #4956) : Le jumeau Python de ce notebook utilise jpype1 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 (6.0 Mo charges a l’init, voir cellule 6 :
Tweety (IKVM) reference chargee : org.tweetyproject.tweety-advanced-logics v1.30.0.0 (6,0 Mo)). Les deux strategies donnent acces au meme API Tweety. Particularite : ce notebook utilise le vrai outil SOTA (IKVM recompilation nativenuget: IKVM, 8.14.0) et documente honêtement les 365IKVM0101warnings du runtime en cellule Conclusion. Audit c.740 (2026-07-22) : 0 doc-honesty finding corrigible des deux cotes (jumeau Python documente en transparence le bug upstream SPASSWriter Issue #1334).
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" : "MISSING"));IKVM home=OK#r "org.tweetyproject.tweety-advanced-logics.dll"// Verification que la DLL chargee expose bien les classes DL cles.
using System.Reflection;
using System.IO;
var tweetyDll = "org.tweetyproject.tweety-advanced-logics.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-advanced-logics v1.30.0.0 (6.0 Mo).2 — Bases de connaissances DL : TBox et ABox
Une base de connaissances DL se decompose en deux parties :
- la TBox (terminological box) declare les concepts et leurs relations : inclusions
A ⊑ B(“tout A est un B”), equivalencesA ≡ B; - la ABox (assertional box) declare les individus : appartenance
a : C(“l’individuaest une instance du conceptC”) ou relationsa R b(“aest en relationRavecb”).
En Tweety, ces deux pieces sont exposees via :
DlBeliefSet: contient a la fois TBox et ABox (structure unifiee) ;DlParser: analyse de strings comme"Human ⊑ Mortal","alice : Human";Concept,Rôle,Individual: noeuds syntaxiques des axiomes.
Pour ce notebook on travaille sur la logique ALC (Attributes Language with Complement) qui admet : - les concepts atomiques A ; - les booléens ⊤ (top), ⊥ (bottom), ¬C (negation), C ⊓ D (intersection), C ⊔ D (union) ; - les restrictions forall R.C et exists R.C.
// Construire des concepts atomiques + compose (Intersection = AND).
using org.tweetyproject.logics.dl.syntax;
var human = new AtomicConcept("Human");
var mortal = new AtomicConcept("Mortal");
var humanMortal = new Intersection(human, mortal);
Console.WriteLine($"Concept compose = {humanMortal}");
// Variables dans la signature : convertir Set -> IEnumerable via java.util.Set methods.
Console.WriteLine($"Variables (predicates) humain = {human.getPredicates()}");Concept compose = (and Human Mortal)
Variables (predicates) humain = [Human(Thing)]Lecture des sorties : le concept composé en notation préfixe
Les deux lignes affichées montrent la surface de l’API DL après build des concepts. Concept compose = (and Human Mortal) — l’intersection s’imprime en notation préfixe (and …), l’usage d’affichage des constructions de concepts : Intersection(human, mortal) est un objet dédié de logics.dl.syntax, pas une concaténation de chaînes — le parser DL de la cellule suivante retrouvera exactement cette forme. La seconde ligne singularise un point d’API : Variables (predicates) humain = [Human(Thing)]. Le prédicat est imprimé avec son arité (Thing) — en logique de descriptions, un concept de base Human est un prédicat unaire, et getPredicates() ramène l’ensemble des symboles de la signature, pas celui des formules. Le commentaire de la cellule signale d’ailleurs le pont technique : la conversion d’java.util.Set vers l’énumération .NET, la friction réelle d’un port IKVM.
// Parser DL : construction KB a partir du format .dlogic canonique.
// Syntaxe officielle (DlParser) :
// signature(:atomic-concepts(C1 C2 ...)
// :roles(R1 R2 ...)
// :individuals(i1 i2 ...))
// implies C D => inclusion TBox (C subsume D)
// instance ind C => ABox assertion (ind est un C)
// related ind1 ind2 R => ABox role assertion
// (cf. exemple canonique "Tweety the bird" / examplebeliefbase.dlogic dans le JAR)
using java.io;
using org.tweetyproject.logics.dl.parser;
using org.tweetyproject.logics.dl.syntax;
var parser = new DlParser();
parser.setSignature(new DlSignature());
var src = @"signature(:atomic-concepts(Bird Mammal Cat Person)
:roles(enemyOf)
:individuals(tweety sylvester))
implies Cat Mammal
instance tweety Bird
instance sylvester Cat";
var bb = parser.parseBeliefBase(new java.io.StringReader(src));
var kb = (DlBeliefSet)bb;
System.Console.WriteLine($"KB DL : {kb.size()} axiomes.");
System.Console.WriteLine($"Signature : {kb.getSignature()}");KB DL : 3 axiomes.
Signature : [Cat, Bird, Mammal], [], [sylvester, tweety]Lecture de la construction de base : trois axiomes, une signature
KB DL : 3 axiomes. recense exactement les trois lignes d’assertion du texte .dlogic : deux instance (tweety Bird, sylvester Cat) et un implies Cat Mammal. Le format est lisible dans la source de la cellule : la signature se déclare en tête (:atomic-concepts, :roles, :individuals), puis les axiomes — implies pour la subsomption TBox, instance pour l’assertion ABox. La sortie Signature aligne trois listes — concepts, rôles, individus — et la liste des rôles imprimée est vide : le format sépare les trois familles de symboles, et seule la signature effective des axiomes est restituée. Enfin le jeu d’individus [sylvester, tweety] répète la paire canonique de la série : ce sont les deux témoins que la section 3 fait raisonner.
3 — Raisonner avec NaiveDlReasoner
NaiveDlReasoner est un raisonneur naif de subsomption et d’instance :
query(DlBeliefSet, Formula)prend une formule DL (concept / axiome) et repond si la KB l’implique (model-theoretic entailment).- Sa complexite est exponentielle (il enumere les interpretations) ; il sert surtout a valider la mechanique, pas pour la production.
Cas pedagogique canonique : 1. KB = { Human ⊑ Mortal, alice : Human } -> alice : Mortal doit etre entail (chainage direct). 2. KB = { ... ABox mentionne alice et bob, ... } -> verifier la consistance (pas d’incoherence sensee).
// Inference canonique "Tweety the bird" : Tweety est un Bird, Bird subsume Animal, doit-on conclure Tweety : Animal ?
using java.io;
using org.tweetyproject.logics.dl.parser;
using org.tweetyproject.logics.dl.syntax;
using org.tweetyproject.logics.dl.reasoner;
var parser = new DlParser();
parser.setSignature(new DlSignature());
// Test 1 : Tweety the bird - Bird subsume Animal (axiome T canonique).
var src1 = @"signature(:atomic-concepts(Bird Animal)
:individuals(tweety))
implies Bird Animal
instance tweety Bird";
var bb1 = parser.parseBeliefBase(new java.io.StringReader(src1));
var kb1 = (DlBeliefSet)bb1;
var q1 = parser.parseFormula(new java.io.StringReader("instance tweety Animal"));
bool entail1 = ((java.lang.Boolean)new NaiveDlReasoner().query(kb1, q1)).booleanValue();
System.Console.WriteLine($"KB1 entail (tweety : Animal via Bird subsume Animal) : {entail1}");
// Test 2 : Sylvester Cat avec TBox Cat subsume Mammal.
var src2 = @"signature(:atomic-concepts(Bird Mammal Cat Animal)
:individuals(tweety sylvester))
implies Bird Animal
implies Cat Mammal
instance tweety Bird
instance sylvester Cat";
var bb2 = parser.parseBeliefBase(new java.io.StringReader(src2));
var kb2 = (DlBeliefSet)bb2;
var q2a = parser.parseFormula(new java.io.StringReader("instance sylvester Mammal"));
var q2b = parser.parseFormula(new java.io.StringReader("instance sylvester Animal"));
bool e2a = ((java.lang.Boolean)new NaiveDlReasoner().query(kb2, q2a)).booleanValue();
bool e2b = ((java.lang.Boolean)new NaiveDlReasoner().query(kb2, q2b)).booleanValue();
System.Console.WriteLine($"KB2 entail (sylvester : Mammal via Cat subsume Mammal) : {e2a}");
System.Console.WriteLine($"KB2 entail (sylvester : Animal, en l'absence de Mammal subsume Animal) : {e2b}");KB1 entail (tweety : Animal via Bird subsume Animal) : True
KB2 entail (sylvester : Mammal via Cat subsume Mammal) : True
KB2 entail (sylvester : Animal, en l'absence de Mammal subsume Animal) : FalseLecture des inférences : trois requêtes, deux vrais, un faux — et pourquoi
Les trois lignes de la cellule se lisent comme un mini-benchmark du raisonneur naïf. Test 1 : tweety : Animal est conclu True grâce à l’axiome implies Bird Animal — la subsomption directe suffit. Test 2 : sylvester : Mammal est conclu True par implies Cat Mammal. Test 3 — celui qui instruit : sylvester : Animal est conclu False en l’absence de implies Mammal Animal. Le raisonneur n’invente pas la transitivité : sans la flèche écrite dans la TBox, la chaîne Cat → Mammal → Animal ne s’infère pas, même si deux subsomptions séparées tiennent. C’est la discipline « le vrai d’une base est ce que la base énonce » : l’ontologie se paie axiome par axiome, et le silence de la sortie sur une conclusion vaut preuve négative.
Exercices
Stubs sans
throw/raise(convention C.1) : le notebook s’execute de bout en bout même non complete.
Exercice 1 — Chaîne de subsomption a 3 niveaux
Construisez une TBox a 3 concepts en chaîne : Salarie ⊑ Personne ; Employe ⊑ Personne. Verifiez avec NaiveDlReasoner.query que Salarie ⊑ Personne est entail, mais que Salarie ⊑ Employe ne l’est pas (ils sont disjoints en termes de subsomption car aucun n’inclut l’autre dans l’autre sens).
Indice : parser.parseFormula("Salarie ⊑ Personne") et parser.parseFormula("Salarie ⊑ Employe") produisent les axiomes a passer au reasoner. Ces chaînes se comparent via ⊑ (subseteq logiques), pas via ≡ (equivalence).
// TODO etudiant : TBox 3 concepts Salarie/Personne/Employe, queryer la subsomption
object entSalariePersonne = null; // TODO etudiant : bool, KB entail (Salarie subsume Personne)
object entSalarieEmploye = null; // TODO etudiant : bool, KB entail (Salarie subsume Employe)
string label1 = entSalariePersonne != null ? entSalariePersonne.ToString() : "Exercice a completer";
string label2 = entSalarieEmploye != null ? entSalarieEmploye.ToString() : "Exercice a completer";
System.Console.WriteLine($"KB entail (Salarie subsume Personne) : {label1}");
System.Console.WriteLine($"KB entail (Salarie subsume Employe) : {label2}");
System.Console.WriteLine("Exercice a completer")
KB entail (Salarie subsume Personne) : Exercice a completer
KB entail (Salarie subsume Employe) : Exercice a completer
Exercice a completerExercice 2 — Rôle et restriction existentielle
Les rôles sont les proprietes binaires en DL. Definissez un rôle hasParent, puis testez si la KB { ∃hasParent.Human ⊑ Parent, alice : Parent } implique qu’il existe un humain lie a alice par hasParent.
Cela suppose de manipuler les axiomes de subsomption, ce que le NaiveDlReasoner gere via parseFormula.
Question : la subsomption ∃hasParent.Human ⊑ Parent dit-elle qu’un Parent est quelqu’un qui a au moins un parent humain. Si alice est un Parent, doit-on conclure qu’il existe un parent humain de alice ?
// TODO etudiant : KB avec restriction existentielle sur role hasParent.
// Definissez la TBox, ajoutez alice : Parent, et queryez : la KB entail-elle "alice : exists hasParent . Human" ?
object existeParentHumain = null; // TODO etudiant : bool (ou null si non complete)
string label = existeParentHumain != null ? existeParentHumain.ToString() : "Exercice a completer";
System.Console.WriteLine($"KB entail (alice : exists hasParent . Human) : {label}");
System.Console.WriteLine("Exercice a completer")
KB entail (alice : exists hasParent . Human) : Exercice a completer
Exercice a completerExercice 3 — Cohabitation exemple + exercice (multi-formules)
Demontrer la cohabitation (cf exercise-example-labeling.md) : ci-dessus on a déjà un exemple resolu (sections 2-3 : chainage direct alice-Mortal). Ajoutez ici un exercice non resolu qui exige l’etudiant de raisonner sur la conjonction de concepts :
Construisez un concept EtudiantSalarie = Human ⊓ Salarie, et testez si une ABox avec alice : EtudiantSalarie est consistante (ne créé pas de contradiction) avec une TBox contenant Human ⊑ Personne.
Indice : Concept.AND(humanConcept, salarieConcept) permet de construire le concept compose, mais ici on peut utiliser directement le parser : "alice : Human ⊓ Salarie" n’est pas une formule DL valide en ALC standard ; utilisez parser.parseBeliefSet ou composez deux formules distinctes.
// TODO etudiant : conjonction de concepts (alice : Human ET alice : Salarie),
// verifier la consistance avec une TBox simple.
object estConsistant = null; // TODO etudiant : bool, KB entail (alice : Human), KB entail (alice : Salarie)
string label = estConsistant != null ? estConsistant.ToString() : "Exercice a completer";
System.Console.WriteLine($"KB entail (alice : Human) : {label}");
System.Console.WriteLine($"KB entail (alice : Salarie) : {label}");
System.Console.WriteLine("Exercice a completer")
KB entail (alice : Human) : Exercice a completer
KB entail (alice : Salarie) : Exercice a completer
Exercice a completerConclusion
On a porte en C#/.NET natif (sans JVM) le module logics-dl de TweetyProject — le sous-ensemble Description Logics (ALC) 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 (ce notebook) : Description Logics (ALC, TBox/ABox, NaiveDlReasoner)
Les DL sont le pont entre logique et representation de connaissances : la syntaxe compacte (concepts, rôles, axiomes) nourrit les ontologies OWL / web sémantique, et fournit un terrain d’exercice pour les raisonneurs specialises.
Pourquoi un raisonneur NaiveDlReasoner ?
Le NaiveDlReasoner enumere completement les interpretations possibles du domaine logique. Sa complexite est exponentielle, donc reservee aux KB pedagogiques de petite taille ; pour la production on utilise des raisonneurs dedies (Pellet, HermiT, ELK) ou des variantes optimisees de Tweety (ShiqReasoner, ElReasoner).
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+). IKVM 8.15.0 ne compile pas integralement ces classes (365 IKVM0101 warnings sur l’opération dotnet build). Les classes DL de surface (DlBeliefSet, DlParser, NaiveDlReasoner, Concept) sont compilees avec succes et directement utilisables. Pour les modules internes (sat4j, FOL, commons-lang3), les classes non compilees apparaissent comme IKVM0100 (not found) ; ceci n’affecte pas le port pedagogique des DL.
References
- Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.). The Description Logic Handbook. Cambridge University Press, 2003.
- TweetyProject — logics-dl module.
- Port C#/.NET via IKVM — EPIC #4667. Et la taille de la DLL complète le tableau du port :
tweety-advanced-logicsse charge à 6,0 Mo (v1.30.0.0, cellule 5) quand ses frères de série affichent 7,0 Mo (ModalLogic), 8,0 Mo (QBF), 11,0 Mo (Conditional) et 13,0 Mo (RPCL) dans les autres notebooks du port — la surface IKVM facturée par module, pas une métrique de richesse logique : DL y ajoute la couche parser.dlogicque les sections 2 et 3 ont fait vivre sans JVM.