Tweety-2c — Logique du premier ordre en C#/.NET (port natif IKVM)

Série Tweety — port C#/.NET natif (EPIC #4667). Ce notebook exploite la librairie Java TweetyProject sans JVM : les modules sont compilés vers du bytecode Java puis exécutés sur le runtime .NET via IKVM. Aucun java n’est requis à l’exécution — tout se passe dans le kernel .net-csharp.

Navigation : Tweety-2-Basic-Logics-Csharp (logique propositionnelle) · Tweety-2b-Semantics-Csharp (mondes possibles, conséquence sémantique) · Tweety-2c-FOL (ce notebook).

Objectifs pédagogiques

La logique propositionnelle raisonne sur des propositions entières (Man_Socrates, Mortal_Socrates) reliées par connecteurs. Elle ne peut ni exprimer la généralité (« tous les hommes sont mortels ») ni le lien interne d’un énoncé (« Socrate est un homme »).

La logique du premier ordre (FOL, first-order logic) introduit :

Concept Rôle Exemple
Terme (Term) Objet du discours la variable X, la constante Socrate
Prédicat (Predicate) Propriété / relation sur les termes Homme(·), Parent(·,·)
Atome (FolAtom) Énoncé atomique Homme(Socrate)
Quantificateur universel ∀ « pour tout » ∀X (Homme(X) ⇒ Mortel(X))
Quantificateur existentiel ∃ « il existe » ∃X Mortel(X)

Ce notebook montre comment construire des formules FOL de façon programmatique en C#, puis raisonner dessus avec le raisonneur d’énumération de Tweety (SimpleFolReasoner) — le célèbre syllogisme de la mortalité de Socrate, jusqu’à la généralisation existentielle.

1 — Runtime IKVM : exécuter Tweety sur .NET

On installe le runtime IKVM (machine virtuelle Java réimplémentée en .NET) à partir des paquets NuGet, puis on pointe IKVM.Home vers une image fusionnée (base any + runtime de la plateforme : win-x64, linux-x64, osx-arm64…). La librairie org.tweetyproject.tweety-pl.dll (compilée côté build) se charge par #r ; elle embarque transitivement le module fol (logique du premier ordre), aucun module supplémentaire à compiler ici.

#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);
Console.WriteLine("IKVM home=" + (File.Exists(Path.Combine(ikvmHome, "lib", "tzdb.dat")) ? "OK" : "MISSING"));

IKVM home=OK
#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).

2 — Signature, termes et atomes

Une signature FOL fixe le vocabulaire : quels prédicats (avec leur arité) et quelles constantes représentent les objets nommés. Les variables (X, Y) dénotent des objets arbitraires ; les constantes (Socrate) dénotent un objet précis. Un atome applique un prédicat à des termes.

2.1 Construire un atome

On importe les espaces de noms Tweety puis on instancie un prédicat unaire et on l’applique à un terme. L’API C# expose les classes Java en PascalCase mais conserve les méthodes Java en minuscules (.add, .size) — c’est la convention de port IKVM.

using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.fol.reasoner;
using org.tweetyproject.logics.fol.parser;

// Un prédicat unaire "Homme" et une variable X
var Homme = new Predicate("Homme", 1);
var X = new Variable("X");

// Atome Homme(X) : le prédicat appliqué à la variable
var hommeX = new FolAtom(Homme, X);
Console.WriteLine("Homme(X)        = " + hommeX);

// Une constante nommée Socrate
var socrate = new Constant("Socrate");
var hommeSocrate = new FolAtom(Homme, socrate);
Console.WriteLine("Homme(Socrate)  = " + hommeSocrate);

Homme(X)        = Homme(X)
Homme(Socrate)  = Homme(Socrate)

2.2 Atomes, prédicats et types de termes

FolAtom accepte une liste variable de termes (Predicate, params Term[]) — l’arité du prédicat doit correspondre au nombre de termes fournis. Term est une interface (...syntax.interfaces.Term) implémentée à la fois par Variable et Constant : un atome est donc polymorphe sur ses arguments.

Pourquoi distinguer Variable et Constant via une interface commune ? C’est ce polymorphisme qui rend l’unification possible — le mécanisme au cœur du raisonnement FOL. Face à la règle Homme(X) ⇒ Mortel(X) et au fait Homme(Socrate), le raisonneur unifie la variable X avec la constante Socrate : il substitue X partout où elle apparaît dans la règle, puis déduit Mortel(Socrate). Une Variable est un trou à remplir (liée par un quantificateur, instanciée à l’unification) ; une Constant est un individu figé (Socrate, Platon). Exposer les deux derrière la même interface Term permet au moteur de manipuler atomes et substitutions sans distinguer les cas : c’est exactement ce que ferait un Prolog ou le raisonner de Tweety en interne.

// Prédicat binaire : Parent(·,·) — arité 2
var Parent = new Predicate("Parent", 2);
var anne = new Constant("Anne");
var bob = new Constant("Bob");
var parentAnneBob = new FolAtom(Parent, anne, bob);
Console.WriteLine("Parent(Anne,Bob) = " + parentAnneBob);

// Une variable peut figurer parmi les arguments (relation "Anne est parent de quelqu'un")
var Y = new Variable("Y");
var parentAnneY = new FolAtom(Parent, anne, Y);
Console.WriteLine("Parent(Anne,Y)   = " + parentAnneY);

Parent(Anne,Bob) = Parent(Anne,Bob)
Parent(Anne,Y)   = Parent(Anne,Y)

3 — Connecteurs et quantificateurs

Les connecteurs propositionnels (Implication, Conjunction, Disjunction, Negation) s’appliquent aux formules FOL exactement comme en logique propositionnelle. La nouveauté est le quantificateur, qui lie une variable à l’intérieur d’une formule :

  • ForallQuantifiedFormula(formule, variable) → ∀X formule
  • ExistsQuantifiedFormula(formule, variable) → ∃X formule

3.1 L’axiome classique : « tous les hommes sont mortels »

∀X (Homme(X) ⇒ Mortel(X)) se construit en emboîtant un Implication dans un ForallQuantifiedFormula.

var Mortel = new Predicate("Mortel", 1);

// Homme(X) ⇒ Mortel(X)
var hommeX = new FolAtom(Homme, X);
var mortelX = new FolAtom(Mortel, X);
var impl = new Implication(hommeX, mortelX);
Console.WriteLine("Homme(X) => Mortel(X) = " + impl);

// ∀X (Homme(X) => Mortel(X))
var tousMortels = new ForallQuantifiedFormula(impl, X);
Console.WriteLine("∀X (Homme(X)=>Mortel(X)) = " + tousMortels);

Homme(X) => Mortel(X) = (Homme(X)=>Mortel(X))
∀X (Homme(X)=>Mortel(X)) = forall X: ((Homme(X)=>Mortel(X)))

3.2 Existential : « il existe un mortel »

∃X Mortel(X) ne quantifie qu’un atome. On réutilise le même atome mortelX (qui porte la variable X).

Pourquoi le quantificateur existentiel compte-t-il ? ∃X Mortel(X) affirme qu’au moins un mortel existe, sans nommer qui. C’est précisément ce gain d’expressiveness qui distingue la logique du premier ordre de la logique propositionnelle : en propositionnel, il faudrait énumérer Mortel(Socrate) ∨ Mortel(Platon) ∨ … — une disjunction finie qui ne capture jamais l’existence en général. L’existential, lui, porte sur le domaine tout entier. Deux conséquences concrètes pour le raisonnement : (1) généralisation existentielle — de Mortel(Socrate) on déduit ∃X Mortel(X) sans connaître les autres mortels ; (2) dualité avec le universel (De Morgan) : ¬∀X P(X) équivaut à ∃X ¬P(X), et ¬∃X P(X) à ∀X ¬P(X). Le raisonneur exploite ces équivalences pour réécrire les négations et déduire des existentiels à partir d’universels.

var existeMortel = new ExistsQuantifiedFormula(mortelX, X);
Console.WriteLine("∃X Mortel(X) = " + existeMortel);

// Négation d'une formule quantifiée : ¬∃X Mortel(X)  ("personne n'est mortel")
var personneMortel = new Negation(existeMortel);
Console.WriteLine("¬∃X Mortel(X) = " + personneMortel);

∃X Mortel(X) = exists X: (Mortel(X))
¬∃X Mortel(X) = !exists X: (Mortel(X))

4 — Raisonnement : le syllogisme

On rassemble les axiomes dans un ensemble de croyances (FolBeliefSet, équivalent FOL du PlBeliefSet propositionnel) puis on interroge le raisonneur.

SimpleFolReasoner procède par énumération des interprétations de Herbrand : il construit l’univers de Herbrand (les constantes apparaissant dans la base) et teste les formules sur les interprétations possibles. C’est complet mais exponentiel — adapté à de petites bases pédagogiques.

Pourquoi énumérer seulement Herbrand suffit-il ? Le théorème de Herbrand garantit qu’une base FOL est insatisfiable si et seulement si un ensemble fini d’instances ground (formules sans variable, obtenues en substituant les constantes aux variables) l’est déjà. Le raisonneur peut donc se limiter aux interprétations sur l’univers de Herbrand — ici {Socrate, Platon} — sans inventer d’individus extérieurs. Le prix de cette généralité se chiffre immédiatement : avec 2 constantes et 2 prédicats unaires, il y a 4 atomes ground possibles (Homme(Socrate), Homme(Platon), Mortel(Socrate), Mortel(Platon)) et donc 2⁴ = 16 interprétations à explorer. Chaque constante ou prédicat ajouté double ou quadruple ce compte : sur une base réelle (centaines de constantes, prédicats d’arité 2+), l’énumération explose exponentiellement — c’est la limite structurelle de cette méthode, formalisée en section 5.

Syllogisme classique. Des prémisses ∀X (Homme(X) ⇒ Mortel(X)) et Homme(Socrate), on infère Mortel(Socrate). En termes de conséquence logique : KB ⊨ Mortal(Socrates).

// Base de croyances : l'axiome universel + le fait Homme(Socrate)
var kb = new FolBeliefSet();
kb.add(tousMortels);
kb.add(new FolAtom(Homme, socrate));

Console.WriteLine("KB = " + kb);
Console.WriteLine("taille KB = " + kb.size());

var r = new SimpleFolReasoner();
var mortelSocrate = new FolAtom(Mortel, socrate);
Console.WriteLine("\nKB ⊨ Mortel(Socrate) ?  " + r.query(kb, mortelSocrate));

KB = { Homme(Socrate), forall X: ((Homme(X)=>Mortel(X))) }
taille KB = 2

KB ⊨ Mortel(Socrate) ?  true

4.1 Contrôle négatif : ce qui n’est pas impliqué

Platon n’apparaît dans aucune prémisse : Homme(Platon) n’est ni affirmé ni inférable. Le raisonneur répond donc false à KB ⊨ Mortel(Platon) — la base est sous-déterminée pour Platon. Ce false signifie « pas conséquence logique », pas « conséquence logique du contraire ».

var platon = new Constant("Platon");
var mortelPlaton = new FolAtom(Mortel, platon);
Console.WriteLine("KB ⊨ Mortel(Platon) ?  " + r.query(kb, mortelPlaton));

// Idem : Homme(Platon) n'est pas impliqué non plus
Console.WriteLine("KB ⊨ Homme(Platon) ?  " + r.query(kb, new FolAtom(Homme, platon)));

KB ⊨ Mortel(Platon) ?  false
KB ⊨ Homme(Platon) ?  false

4.2 Généralisation existentielle

Si Mortel(Socrate) est conséquence, alors ∃X Mortel(X) l’est aussi : il existe au moins un mortel (Socrate). C’est la règle d’introduction du quantificateur existentiel. Le raisonneur le confirme directement sur la formule quantifiée.

Console.WriteLine("KB ⊨ ∃X Mortel(X) ?  " + r.query(kb, existeMortel));

// Symétriquement, ∀X Mortel(X) n'est PAS impliqué : seuls les hommes connus le sont
var tousMortels2 = new ForallQuantifiedFormula(mortelX, X);
Console.WriteLine("KB ⊨ ∀X Mortel(X) ?    " + r.query(kb, tousMortels2));

KB ⊨ ∃X Mortel(X) ?  true
KB ⊨ ∀X Mortel(X) ?    false

Lecture des deux réponses. L’asymétrie ∃X Mortel(X) → true / ∀X Mortel(X) → false est instructive : la première est portée par un témoin (Socrate suffit — le fait Homme(Socrate) plus l’axiome universel produit Mortel(Socrate), et le lemme d’introduction existentielle fait le reste), tandis que la seconde exigerait que tous les individus de l’univers de Herbrand soient mortels — or la base ne dit rien de Platon (aucun Homme(Platon) dans kb), et une seule interprétation de Herbrand où Mortel(Platon) est faux suffit à casser l’universel. Retenez la règle de lecture : l’existential est facile à prouver (un témoin), l’universel est facile à réfuter (un contre-exemple) — et symétriquement difficile dans l’autre sens. C’est exactement cette asymétrie qui rend le FOL semi-décidable (section 5).

4.3 Une KB plus riche : raisonnement sur plusieurs faits

Ajoutons un second fait Homme(Platon) et un prédicat Grec. On vérifie que le syllogisme se propage à tous les hommes connus, et qu’un énoncé mixte ∃X (Grec(X) ∧ Mortel(X)) devient conséquence dès qu’au moins un Grec mortel est dans la base.

var Grec = new Predicate("Grec", 1);
var kb2 = new FolBeliefSet();
kb2.add(tousMortels);                       // ∀X (Homme(X) => Mortel(X))
kb2.add(new FolAtom(Homme, socrate));       // Homme(Socrate)
kb2.add(new FolAtom(Homme, platon));        // Homme(Platon)
kb2.add(new FolAtom(Grec, socrate));        // Grec(Socrate)

Console.WriteLine("KB2 ⊨ Mortel(Socrate) ? " + r.query(kb2, new FolAtom(Mortel, socrate)));
Console.WriteLine("KB2 ⊨ Mortel(Platon) ?  " + r.query(kb2, new FolAtom(Mortel, platon)));

// ∃X (Grec(X) ∧ Mortel(X)) : "il existe un Grec mortel"
var grecX = new FolAtom(Grec, X);
var existeGrecMortel = new ExistsQuantifiedFormula(
    new Conjunction(grecX, mortelX), X);
Console.WriteLine("KB2 ⊨ ∃X (Grec(X) ∧ Mortel(X)) ? " + r.query(kb2, existeGrecMortel));

KB2 ⊨ Mortel(Socrate) ? true
KB2 ⊨ Mortel(Platon) ?  true
KB2 ⊨ ∃X (Grec(X) ∧ Mortel(X)) ? true

Lecture des trois réponses. Mortel(Socrate) et Mortel(Platon) : le syllogisme se propage à chaque fait Homme(·) ajouté — le raisonner généralise l’axiome universel à chaque constante de l’univers, par unification. La troisième requête est la plus intéressante : ∃X (Grec(X) ∧ Mortel(X)) vaut true parce que le témoin est Socrate, cumulant Grec(Socrate) (fait) et Mortel(Socrate) (inférence). Le test de contrôle mental : retirez Grec(Socrate) de la base — l’existential retombe à false, alors même que tous les mortels sont toujours là. La conjonction sous quantificateur est donc plus exigeante que la somme de ses parties : KB ⊨ ∃X Grec(X) et KB ⊨ ∃X Mortel(X) peuvent être vrais ensemble sans que KB ⊨ ∃X (Grec(X) ∧ Mortel(X)) le soit — les deux témoins peuvent être des individus différents.

5 — Sémantique ouverte, complexité, et ce que FOL ne décide pas

5.1 Monde ouvert : le false du raisonner n’est pas un « non »

Le contrôle négatif de la section 4.1 mérite sa généralisation. En logique du premier ordre, une base de croyances fonctionne en monde ouvert (Open World Assumption) : ce qui n’est pas démontrable est inconnu, jamais faux. Ce choix s’oppose à l’hypothèse du monde fermé (Closed World Assumption) des bases de données : si une ligne Mortel(Platon) est absente d’une table SQL, le système conclut « Platon n’est pas mortel » ; face à la même lacune, SimpleFolReasoner répond false à KB ⊨ Mortel(Platon) — c’est-à-dire « pas conséquence », et répond aussi false à KB ⊨ ¬Mortel(Platon). Aucun des deux n’est connu. Le FOL est conçu pour raisonner sur des connaissances incomplètes par nature (il peut exister des mortels que la base ne nomme pas) ; une base de données est conçue pour gérer des états complets par convention. Confondre les deux sémantiques est l’erreur classique du débutant : importer un dump SQL dans un raisonner FOL et s’attendre à des réponses par négation échoue systématiquement.

5.2 Le prix de la généralité : exponentiel en pratique, indécidable en théorie

Deux limites emboîtées. En pratique, l’énumération de Herbrand (section 4) coûte 2^(nombre d'atomes ground) — SimpleFolReasoner est borné aux petites bases pédagogiques ; les raisonneurs industriels n’énumèrent pas, ils dérivent par résolution + unification (le mécanisme entrevu en 2.2), ce qui évite d’explorer tout l’espace d’interprétations mais ne fait qu’atténuer l’explosion. En théorie, le problème de fond est plus grave : la validité FOL est semi-décidable (théorème de Church-Turing, 1936). Si une formule est valide, une procédure correcte la prouvera en temps fini ; si elle ne l’est pas, la même procédure peut boucler indéfiniment sans jamais répondre. L’asymétrie ∃/∀ de la section 4.2 en est la manifestation concrète : prouver un existential demande un témoin (recherche finie), réfuter un universel demande l’absence de contre-exemple sur un domaine potentiellement infini — aucune machine ne peut certifier cette absence en général. C’est pourquoi la question « cette KB est-elle consistante ? » n’a pas d’algorithme général qui termine toujours — et pourquoi l’exercice 3 (détection d’inconsistance) travaille sur un cas où le raisonner répond vite : la contradiction y est posée en faits ground, sans quantificateur à instancier.

5.3 Et ensuite

Ce notebook couvre la syntaxe FOL et le raisonnement sémantique par énumération. Trois suites naturelles dans la série : Tweety-3-Advanced-Logics-Csharp (logiques modales et conditionnelles, qui restreignent la quantification pour regagner de la décidabilité), le notebook Tweety-5-Abstract-Argumentation-Csharp (le FOL y devient le langage des arguments, la contradiction cesse d’être une pathologie pour devenir l’objet d’étude), et l’exercice 3 ci-dessous qui montre pourquoi l’inconsistance doit être traquée avant tout raisonnement sérieux.

Exercices

Les exercices sont à compléter. Conformément à la convention du dépôt, les stubs ne lèvent jamais d’erreur (raise/throw interdits) : ils retournent null / affichent un message. Le notebook s’exécute donc de bout en bout même non complété.

Exercice 1 — Le chat mammifère

Construisez programmatiquement l’axiome ∀X (Chat(X) ⇒ Mammifère(X)), ajoutez le fait Chat(Felix), puis vérifiez que KB ⊨ Mammifère(Felix) vaut true. Créez les prédicats Chat et Mammifère (arité 1) et la constante Felix.

// TODO etudiant : construire la base et le raisonneur
// Indice : suivez la structure de la section 4 (Predicate, Constant, FolAtom, Implication,
//          ForallQuantifiedFormula, FolBeliefSet.add, SimpleFolReasoner.query).
// Etape 1 : déclarer les prédicats Chat / Mammifere et la constante Felix.
// Etape 2 : construire ∀X (Chat(X) => Mammifere(X)) et Chat(Felix).
// Etape 3 : interroger KB |= Mammifere(Felix).
bool? reponse = null;  // TODO etudiant : affecter le resultat de la requete
Console.WriteLine("KB ⊨ Mammifere(Felix) ? " + (reponse?.ToString() ?? "Exercice a completer"));

KB ⊨ Mammifere(Felix) ? Exercice a completer

Correction guidée — Exercice 1

La solution suit cinq gestes, tous déjà rencontrés : (1) new Predicate("Chat", 1) et new Predicate("Mammifere", 1) ; (2) new Constant("Felix") ; (3) l’implication Chat(X) ⇒ Mammifere(X) par new Implication sur deux FolAtom partageant la même variable X — c’est le partage de variable qui porte le sens de la règle ; (4) le quantificateur new ForallQuantifiedFormula(impl, X) ; (5) FolBeliefSet + SimpleFolReasoner.query. L’erreur type : omettre le geste (4) et ajouter l’implication non quantifiée à la base. Qu’observerait-on alors ? L’implication nue contient une variable libre — l’énumération de Herbrand l’instancie sur Felix, et la requête Mammifere(Felix) répond quand même true. La base « fonctionne » sans l’universel parce que l’univers est réduit à un seul individu. Le bug est invisible ici et mortel dès qu’une seconde constante entre en scène : ajoutez Chat(Milou) — sans le ∀X, rien ne pousse à conclure Mammifere(Milou). C’est le cas d’école pour comprendre que le quantificateur n’est pas une décoration syntaxique : c’est lui qui étend la règle à l’univers entier.

Exercice 2 — Transitivité : grand-parent

Avec un prédicat binaire Parent(·,·), on veut définir « grand-parent » sans nouveau prédicat : ∀X ∀Y ∀Z (Parent(X,Y) ∧ Parent(Y,Z) ⇒ GrandParent(X,Z)). Construisez cette formule à partir de deux quantificateurs universels emboîtés et affichez-la.

Indice : ForallQuantifiedFormula ne lie qu’une variable à la fois ; pour ∀X ∀Y ∀Z il faut emboîter trois constructeurs (le plus externe lie Z, l’intermédiaire lie Y, l’interne lie X).

// TODO etudiant : construire la formule GrandParent
// Indice : declarez Z = new Variable("Z"); construisez l'implication,
//          puis ForallQuantifiedFormula(... X) dans ForallQuantifiedFormula(... Y) dans ForallQuantifiedFormula(... Z).
object formuleGrandParent = null;  // TODO etudiant
Console.WriteLine("GrandParent = " + (formuleGrandParent?.ToString() ?? "Exercice a completer"));

GrandParent = Exercice a completer

Correction guidée — Exercice 2

L’emboîtement : la formule n’introduit pas de prédicat GrandParent dédié — elle définit la relation transitive de grand-parenté par pure contrainte logique sur Parent. Trois ForallQuantifiedFormula emboîtés, du plus interne (lie X) au plus externe (lie Z) : ∀Z(∀Y(∀X(…))). Deux points de sémantique à ne pas rater. (a) L’ordre importe — sauf entre universels : ∀X ∀Y φ et ∀Y ∀X φ sont équivalents (une succession de universels commute), donc les trois emboîtements peuvent s’écrire dans n’importe quel ordre entre eux. Ce privilège s’arrête aux quantificateurs homogènes : ∀X ∃Y Parent(X,Y) (« chacun a un parent ») et ∃Y ∀X Parent(X,Y) (« quelqu’un est le parent de tous ») disent des choses radicalement différentes — dans le second, le même témoin Y doit servir tous les X. L’exercice n’utilise que des universels, mais dès que vous mélangerez (section 3), retenez : le quantificateur externe choisit le premier, et l’interne choisit en connaissant le choix de l’externe. (b) La forme prénexe : toute formule FOL est équivalente à une formule où tous les quantificateurs sont en tête (∀X ∀Y ∀Z (…) — exactement la forme demandée ici) ; la conversion (déplacer les quantificateurs à travers ¬, ∧, ∨ en utilisant les dualités de De Morgan vues en 3.2) est standard mais ne commute pas les quantificateurs entre eux.

Exercice 3 — Détection d’inconsistance

Une base est inconsistante si elle implique une contradiction (ex. à la fois P(a) et ¬P(a)). Avec SimpleFolReasoner, une KB inconsistante implique toute formule (ex falso quodlibet).

Ajoutez à une KB les faits Mortel(Socrate) et ¬Mortel(Socrate), puis vérifiez que KB ⊨ Homme(Socrate) vaut true (principe d’explosion) — bien qu’aucun axiome ne parle d’Homme.

// TODO etudiant : mettre en evidence le principe d'explosion
// Indice : kb.add(FolAtom Mortel(Socrate)) ; kb.add(new Negation(FolAtom Mortel(Socrate))).
//          Puis interrogez KB |= Homme(Socrate) sur un prédicat Homme non lie par vos axiomes.
bool? explosion = null;  // TODO etudiant
Console.WriteLine("KB inconsistante ⊨ Homme(Socrate) ? " + (explosion?.ToString() ?? "Exercice a completer"));

KB inconsistante ⊨ Homme(Socrate) ? Exercice a completer

Correction guidée — Exercice 3

La mécanique : KB = {Mortel(Socrate), ¬Mortel(Socrate)}, puis query(kb, Homme(Socrate)) sur un prédicat qu’aucun axiome ne mentionne — et la réponse est true. Pourquoi l’énumération de Herbrand confirme-t-elle l’explosion ? KB ⊨ φ signifie « toute interprétation qui satisfait KB satisfait φ ». Une base contradictoire n’a aucune interprétation qui la satisfait — l’ensemble des modèles de KB est vide, et « tout élément de l’ensemble vide vérifie φ » est trivialement vrai (c’est la vacuité de l’implication sur le vide). Ex falso quodlibet : du faux, tout suit. La leçon opérationnelle dépasse l’exercice : une KB inconsistante prouve tout, y compris les énoncés absurdes — un raisonner branché sur une base contradictoire est un générateur de confiance fausse. C’est pourquoi tout système sérieux (moteur de règles métier, agent dialoguant, base d’arguments) commence par un test de consistance, et pourquoi la série Tweety-5 (argumentation) retourne le problème : plutôt que d’éradiquer la contradiction, elle en fait l’objet d’étude — deux arguments opposés ne font pas exploser le système, ils s’affrontent.

Conclusion

On a porté en C#/.NET natif (sans JVM) le raisonnement du premier ordre via Tweety/IKVM :

  1. Construction programmatique des formules FOL — termes (Variable/Constant), prédicats (Predicate), atomes (FolAtom), connecteurs (Implication/Conjunction/Negation), quantificateurs (ForallQuantifiedFormula/ExistsQuantifiedFormula).
  2. Raisonnement sémantique par énumération de Herbrand (SimpleFolReasoner.query) — le syllogisme ∀X (Homme(X) ⇒ Mortel(X)), Homme(Socrate) ⊨ Mortel(Socrate), le contrôle négatif, la généralisation existentielle, et une KB multi-faits.

FOL vs propositionnel — ce que FOL apporte

Aspect Propositionnel (Tweety-2) Premier ordre (ce notebook)
Objets du discours propositions atomiques entières termes (variables + constantes)
Généralité impossible ∀ (pour tout)
Existence impossible ∃ (il existe)
Structure interne d’un énoncé plate prédicat appliqué à des termes
Raisonneur tables de vérité / mondes énumération de Herbrand

Références

Retour au sommet