SL-4 — Programmation Logique Inductive (ILP) — Twin C# (FOIL from-scratch)

Twin C# (.NET Interactive) de SL-4-InductiveLogicProgramming — marathon #4956 (parité .NET ⇄ Python), série SymbolicLearning, axe-2 SOTA #3801 Prong B.

Le notebook Python déroule l’ILP from-scratch (clauses Horn, unification, FOIL, résolution inverse) sur stdlib pur, puis invoque Popper (la librairie SOTA d’ILP via ASP/CLINGO + Prolog, Linux/WSL-only). Ce twin porte tout le moteur from-scratch en C# (.NET 9, 0 NuGet) : la partie Popper n’a pas d’équivalent .NET (verdict INTRINSIC, documenté honnêtement en fin de notebook).

Objectifs d’apprentissage

1. Représenter des relations en clauses Horn et unifier des littéraux (substitution θ).
2. Implémenter FOIL (ILP top-down, Quinlan 1990) : sélection des littéraux par gain d’information.
3. Appliquer la résolution inverse (ILP bottom-up) : opérateurs V (absorption) et W (identification).
4. Apprendre une règle récursive sur le problème classique des ancêtres ancestor(X, Y).
5. Découvrir des règles ILP sur un mini Knowledge Graph (symétrie, transitivité).

Introduction

Pourquoi l’ILP ?

L’apprentissage propositionnel (SL-1 à SL-3) apprend des conjonctions d’attributs fixes. Mais la connaissance du monde réel est relationnelle : « X est parent de Y », « si X est ancêtre de Y et Y de Z, alors X est ancêtre de Z ». La Programmation Logique Inductive (ILP, AIMA §19.5) apprend de telles règles logiques du premier ordre (clauses Horn) à partir d’exemples positifs/négatifs et d’un background knowledge.

Deux familles d’algorithmes

Approche	Direction	Algorithme emblématique
Top-down	Général → spécifique (on spécialise)	FOIL (Quinlan 1990)
Bottom-up	Spécifique → général (on généralise)	Résolution inverse (Muggleton 1987), opérateurs V/W

FOIL part d’une règle vide et ajoute des littéraux pour réduire les négatifs couverts (gain d’information). La résolution inverse part de faits et absorbe (V) ou combine (W) des clauses pour généraliser.

Complémentarité (#3801)

Aspect	Python (twin)	Twin C# (ici)
Moteur from-scratch	stdlib (dataclass)	record C# + BCL, 0 NuGet
SOTA ILP	Popper (ASP + Prolog)	SOTA-OK : pont clingo Process.Start (§9)

1. Clauses Horn et unification

Un littéral = predicat(arg1, arg2, ...) éventuellement nié. Convention (suivie par le twin Python) : un argument en minuscule est une variable, en majuscule une constante. Une clause Horn = une tête (head) et un corps (body de littéraux) : head :- body1, body2, ... (« si body alors head »).

L’unification trouve une substitution θ rendant deux littéraux opposés compatibles (résolution). C’est le moteur de toute déduction en logique du premier ordre.

#nullable enable
// Cellule 1 — Literal, HornClause, unification (persistant cross-cell .net-csharp)
using System;
using System.Collections.Generic;
using System.Linq;

public record Literal(string Predicate, string[] Args, bool Negated = false)
{
    public bool IsGround => Args.All(a => char.IsUpper(a[0]));          // toutes constantes
    public HashSet<string> Variables => Args.Where(a => char.IsLower(a[0])).ToHashSet();
    public override string ToString() => (Negated ? "~" : "") + Predicate + "(" + string.Join(", ", Args) + ")";
    public virtual bool Equals(Literal? other) =>
        other is not null && Predicate == other.Predicate && Negated == other.Negated && Args.SequenceEqual(other.Args);
    public override int GetHashCode()
    {
        var h = new HashCode(); h.Add(Predicate); h.Add(Negated);
        foreach (var a in Args) h.Add(a); return h.ToHashCode();
    }
    public Literal WithArgs(string[] newArgs) => new Literal(Predicate, newArgs, Negated);
    public Literal WithNegated(bool neg) => new Literal(Predicate, Args, neg);
}

public record HornClause(Literal Head, List<Literal> Body)
{
    public override string ToString() =>
        Body.Count == 0 ? $"{Head}." : $"{Head} :- {string.Join(", ", Body)}.";
    public HashSet<string> Variables()
    {
        var s = Head.Variables;
        foreach (var l in Body) s.UnionWith(l.Variables);
        return s;
    }
}

// --- Unification (substitution : Dictionary<string,string>) ---
public static Dictionary<string,string>? UnifyVar(string v, string term, Dictionary<string,string> subst)
{
    if (subst.TryGetValue(v, out var bound)) return UnifyTerm(bound, term, subst);
    if (subst.TryGetValue(term, out var bound2)) return UnifyTerm(v, bound2, subst);
    if (v == term) return subst;
    var ns = new Dictionary<string,string>(subst); ns[v] = term; return ns;
}

public static Dictionary<string,string>? UnifyTerm(string t1, string t2, Dictionary<string,string> subst)
{
    if (subst.TryGetValue(t1, out var b1)) return UnifyTerm(b1, t2, subst);
    if (subst.TryGetValue(t2, out var b2)) return UnifyTerm(t1, b2, subst);
    if (t1 == t2) return subst;
    if (char.IsLower(t1[0])) return UnifyVar(t1, t2, subst);
    if (char.IsLower(t2[0])) return UnifyVar(t2, t1, subst);
    return null;   // deux constantes differentes
}

public static Dictionary<string,string>? Unify(Literal l1, Literal l2, Dictionary<string,string>? subst = null)
{
    subst ??= new Dictionary<string,string>();
    if (l1.Predicate != l2.Predicate || l1.Args.Length != l2.Args.Length) return null;
    if (l1.Negated == l2.Negated) return null;   // meme signe : pas de resolution
    var result = new Dictionary<string,string>(subst);
    for (int i = 0; i < l1.Args.Length; i++)
    {
        result = UnifyTerm(l1.Args[i], l2.Args[i], result);
        if (result is null) return null;
    }
    return result;
}

// --- Exemples ---
"Representation et unification".Display();
new string('=', 55).Display();
var parentAb = new HornClause(new Literal("parent", new[]{"Alice","Bob"}), new List<Literal>());
$"Fait       : {parentAb}".Display();
var ancParent = new HornClause(new Literal("ancestor", new[]{"x","y"}), new List<Literal>{ new Literal("parent", new[]{"x","y"}) });
$"Regle      : {ancParent}".Display();
var ancRec = new HornClause(new Literal("ancestor", new[]{"x","y"}), new List<Literal>{ new Literal("parent", new[]{"x","z"}), new Literal("ancestor", new[]{"z","y"}) });
$"Recursive  : {ancRec}".Display();
"".Display();
"Unification :".Display();
var s1 = Unify(new Literal("parent", new[]{"x","y"}, false), new Literal("parent", new[]{"Alice","Bob"}, true));
$"  unify(parent(x,y), ~parent(Alice,Bob)) = {{{(s1 is null ? "" : string.Join(", ", s1.Select(kv => $"{kv.Key}={kv.Value}")))}}}".Display();
var s2 = Unify(new Literal("parent", new[]{"x","y"}, false), new Literal("parent", new[]{"x","Bob"}, true));
$"  unify(parent(x,y), ~parent(x,Bob)) = {{{(s2 is null ? "" : string.Join(", ", s2.Select(kv => $"{kv.Key}={kv.Value}")))}}}".Display();

The below script needs to be able to find the current output cell; this is an easy method to get it.

Representation et unification

=======================================================

Fait       : parent(Alice, Bob).

Regle      : ancestor(x, y) :- parent(x, y).

Recursive  : ancestor(x, y) :- parent(x, z), ancestor(z, y).

Unification :

  unify(parent(x,y), ~parent(Alice,Bob)) = {x=Alice, y=Bob}

  unify(parent(x,y), ~parent(x,Bob)) = {y=Bob}

2. Briques de FOIL

FOIL (First-Order Inductive Learner) apprend une clause en ajoutant itérativement des littéraux au corps pour réduire les exemples négatifs couverts, mesurés par un gain d’information à la Quinlan.

• EvaluateLiteral : un littéral ground est vrai s’il est (ou n’est pas) dans le background.
• CheckClauseCovers : énumère toutes les substitutions des variables, vérifie le corps, et retourne les exemples distincts (positifs/négatifs) couverts. Le dédoublonnage sur le tuple-cible est crucial (sinon un littéral comme parent(x,z) paraît faussement meilleur en multipliant les bindings).
• FoilGain : gain = \(p_n \cdot (\log_2 \frac{p_n}{p_n+n_n} - \log_2 \frac{p_0}{p_0+n_0})\) où \(p_0, n_0\) sont les positifs/négatifs avant, \(p_n, n_n\) après.

// Cellule 2 — Briques FOIL (EvaluateLiteral, CheckClauseCovers, FoilGain)
// Background : ensemble de (predicate, args[]) faits connus.
using System.Collections.Generic;
using System.Linq;

public static bool EvaluateLiteral(Literal lit, Dictionary<string,string> binding, HashSet<(string Pred, string[] Args)> background)
{
    var ground = lit.Args.Select(a => binding.GetValueOrDefault(a, a)).ToArray();
    // ATTENTION : string[] = egalite par reference => HashSet.Contains ne matche jamais.
    // Lookup value-based (SequenceEqual) sur le petit background (quelques faits).
    bool inBg = background.Any(f => f.Pred == lit.Predicate && f.Args.SequenceEqual(ground));
    return lit.Negated ? !inBg : inBg;
}

// Produit cartesien des variables -> constantes (toutes les substitutions)
public static IEnumerable<Dictionary<string,string>> AllBindings(string[] vars, string[] constants)
{
    int n = vars.Length;
    if (n == 0) { yield return new Dictionary<string,string>(); yield break; }
    var idx = new int[n];
    int choices = constants.Length;
    while (true)
    {
        var b = new Dictionary<string,string>();
        for (int i = 0; i < n; i++) b[vars[i]] = constants[idx[i]];
        yield return b;
        int k = n - 1;
        while (k >= 0) { idx[k]++; if (idx[k] < choices) break; idx[k] = 0; k--; }
        if (k < 0) yield break;
    }
}

public static (HashSet<(string X, string Y)> posCov, HashSet<(string X, string Y)> negCov) CheckClauseCovers(
    List<Literal> body, string targetPred, string[] targetArgs,
    string[] constants, HashSet<(string Pred, string[] Args)> background,
    HashSet<(string X, string Y)> positives, HashSet<(string X, string Y)> negatives)
{
    // variables du body + cible (minuscules)
    var varSet = new HashSet<string>();
    foreach (var lit in body) foreach (var a in lit.Args) if (char.IsLower(a[0])) varSet.Add(a);
    foreach (var a in targetArgs) if (char.IsLower(a[0])) varSet.Add(a);
    var vars = varSet.OrderBy(v => v).ToArray();

    var posCov = new HashSet<(string, string)>();
    var negCov = new HashSet<(string, string)>();
    foreach (var binding in AllBindings(vars, constants))
    {
        bool ok = body.All(lit => EvaluateLiteral(lit, binding, background));
        if (!ok) continue;
        string tx = binding.GetValueOrDefault(targetArgs[0], targetArgs[0]);
        string ty = binding.GetValueOrDefault(targetArgs[1], targetArgs[1]);
        var key = (tx, ty);
        if (positives.Contains(key)) posCov.Add(key);
        else if (negatives.Contains(key)) negCov.Add(key);
    }
    return (posCov, negCov);
}

public static double FoilGain(int oldPos, int oldNeg, int newPos, int newNeg)
{
    if (newPos == 0) return double.NegativeInfinity;
    int oldTotal = oldPos + oldNeg, newTotal = newPos + newNeg;
    if (oldTotal == 0 || newTotal == 0) return 0.0;
    double oldEntropy = oldPos > 0 ? Math.Log2((double)oldPos / oldTotal) : double.NegativeInfinity;
    double newEntropy = Math.Log2((double)newPos / newTotal);
    return newPos * (newEntropy - oldEntropy);
}

"Fonctions FOIL definies : EvaluateLiteral, AllBindings, CheckClauseCovers, FoilGain".Display();
"".Display();
"Exemples de gain FOIL :".Display();
$"  10 pos / 5 neg -> 8 pos / 1 neg : {FoilGain(10,5,8,1):F3}".Display();
$"  10 pos / 5 neg -> 9 pos / 4 neg : {FoilGain(10,5,9,4):F3}".Display();
$"  10 pos / 5 neg -> 0 pos / 0 neg : {FoilGain(10,5,0,0):F3} (elimine)".Display();

Fonctions FOIL definies : EvaluateLiteral, AllBindings, CheckClauseCovers, FoilGain

Exemples de gain FOIL :

  10 pos / 5 neg -> 8 pos / 1 neg : 3,320

  10 pos / 5 neg -> 9 pos / 4 neg : 0,490

  10 pos / 5 neg -> 0 pos / 0 neg : -∞ (elimine)

3. Le problème des ancêtres

Problème classique d’ILP : apprendre ancestor(X, Y) à partir de faits parent/2. On donne une famille sur 3 générations (Arthur → Bob/Catherine → Diana/Eve → Frank), des exemples positifs (tous les couples ancêtre vrais) et négatifs (couples non-ancêtre). L’objectif : redécouvrir les règles

\[\text{ancestor}(x,y) :- \text{parent}(x,y). \quad \text{ancestor}(x,y) :- \text{parent}(x,z), \text{ancestor}(z,y).\]

// Cellule 3 — Le probleme ancestor(X, Y)
public static HashSet<(string Pred, string[] Args)> BACKGROUND = new() {
    ("parent", new[]{"Arthur","Bob"}),
    ("parent", new[]{"Arthur","Catherine"}),
    ("parent", new[]{"Bob","Diana"}),
    ("parent", new[]{"Catherine","Eve"}),
    ("parent", new[]{"Eve","Frank"}),
};
public static string[] CONSTANTS = new[]{ "Arthur", "Bob", "Catherine", "Diana", "Eve", "Frank" };
public static HashSet<(string X, string Y)> POSITIVES = new() {
    ("Arthur","Bob"), ("Arthur","Catherine"), ("Bob","Diana"), ("Catherine","Eve"), ("Eve","Frank"),
    ("Arthur","Diana"), ("Arthur","Eve"), ("Arthur","Frank"), ("Catherine","Frank"),
};
public static HashSet<(string X, string Y)> NEGATIVES = new() {
    ("Bob","Arthur"), ("Catherine","Arthur"), ("Diana","Bob"), ("Eve","Catherine"),
    ("Frank","Eve"), ("Diana","Arthur"), ("Bob","Catherine"), ("Catherine","Bob"),
    ("Diana","Eve"), ("Eve","Diana"),
};

"Probleme ancestor(X, Y)".Display();
new string('=', 50).Display();
$"Background : {BACKGROUND.Count} faits parent/2".Display();
$"Positifs : {POSITIVES.Count} couples ancestor".Display();
$"Negatifs : {NEGATIVES.Count} couples non-ancestor".Display();
"".Display();
"Familles :".Display();
foreach (var (pred, args) in BACKGROUND.OrderBy(t => t.Args[0]))
    $"  parent({args[0]}, {args[1]})".Display();

Probleme ancestor(X, Y)

==================================================

Background : 5 faits parent/2

Positifs : 9 couples ancestor

Negatifs : 10 couples non-ancestor

Familles :

  parent(Arthur, Bob)

  parent(Arthur, Catherine)

  parent(Bob, Diana)

  parent(Catherine, Eve)

  parent(Eve, Frank)

4. Évaluation de clauses candidates

On teste 3 clauses candidates et leur gain FOIL. La clause récursive ancestor(x,y) :- parent(x,z), ancestor(z,y) nécessite une extension de la cible (les positifs connus) pour évaluer le littéral récursif ancestor(z,y) — procédé standard de FOIL pour les prédicats récursifs.

// Cellule 4 — Clauses candidates pour ancestor
// Extension du background avec les ancetres directs (pour evaluer la recursion)
public static HashSet<(string Pred, string[] Args)> BgWithDirectAncestors()
{
    var bg = new HashSet<(string, string[])>(BACKGROUND);
    foreach (var p in POSITIVES)
        if (p == ("Arthur","Bob") || p == ("Arthur","Catherine") || p == ("Bob","Diana")
            || p == ("Catherine","Eve") || p == ("Eve","Frank"))
            bg.Add(("ancestor", new[]{ p.Item1, p.Item2 }));
    return bg;
}

"FOIL --- Recherche de regles pour ancestor(x, y)".Display();
new string('=', 55).Display();
"".Display();

// Candidate 1 : ancestor(x,y) :- parent(x,y).
var (cp1, cn1) = CheckClauseCovers(new List<Literal>{ new Literal("parent", new[]{"x","y"}) },
    "ancestor", new[]{"x","y"}, CONSTANTS, BACKGROUND, POSITIVES, NEGATIVES);
"Clause : ancestor(x, y) :- parent(x, y).".Display();
$"  Couvre {cp1.Count} positifs : [{string.Join(", ", cp1.OrderBy(p=>p.X).Take(5))}]...".Display();
$"  Couvre {cn1.Count} negatifs : [{string.Join(", ", cn1.OrderBy(p=>p.X).Take(5))}]...".Display();
$"  Gain FOIL : {FoilGain(POSITIVES.Count, NEGATIVES.Count, cp1.Count, cn1.Count):F3}".Display();
"".Display();

// Candidate 2 : ancestor(x,y) :- parent(x,z), parent(z,y).
var (cp2, cn2) = CheckClauseCovers(new List<Literal>{ new Literal("parent", new[]{"x","z"}), new Literal("parent", new[]{"z","y"}) },
    "ancestor", new[]{"x","y"}, CONSTANTS, BACKGROUND, POSITIVES, NEGATIVES);
"Clause : ancestor(x, y) :- parent(x, z), parent(z, y).".Display();
$"  Couvre {cp2.Count} positifs : [{string.Join(", ", cp2.OrderBy(p=>p.X).Take(5))}]...".Display();
$"  Couvre {cn2.Count} negatifs".Display();
$"  Gain FOIL : {FoilGain(POSITIVES.Count, NEGATIVES.Count, cp2.Count, cn2.Count):F3}".Display();
"".Display();

// Candidate 3 (recursive) : ancestor(x,y) :- parent(x,z), ancestor(z,y).
var (cp3, cn3) = CheckClauseCovers(new List<Literal>{ new Literal("parent", new[]{"x","z"}), new Literal("ancestor", new[]{"z","y"}) },
    "ancestor", new[]{"x","y"}, CONSTANTS, BgWithDirectAncestors(), POSITIVES, NEGATIVES);
"Clause : ancestor(x, y) :- parent(x, z), ancestor(z, y). [recursive]".Display();
$"  Couvre {cp3.Count} positifs : [{string.Join(", ", cp3.OrderBy(p=>p.X).Take(5))}]...".Display();
$"  Couvre {cn3.Count} negatifs".Display();
$"  Gain FOIL : {FoilGain(POSITIVES.Count, NEGATIVES.Count, cp3.Count, cn3.Count):F3}".Display();

FOIL --- Recherche de regles pour ancestor(x, y)

=======================================================

Clause : ancestor(x, y) :- parent(x, y).

  Couvre 5 positifs : [(Arthur, Bob), (Arthur, Catherine), (Bob, Diana), (Catherine, Eve), (Eve, Frank)]...

  Couvre 0 negatifs : []...

  Gain FOIL : 5,390

Clause : ancestor(x, y) :- parent(x, z), parent(z, y).

  Couvre 3 positifs : [(Arthur, Diana), (Arthur, Eve), (Catherine, Frank)]...

  Couvre 0 negatifs

  Gain FOIL : 3,234

Clause : ancestor(x, y) :- parent(x, z), ancestor(z, y). [recursive]

  Couvre 3 positifs : [(Arthur, Diana), (Arthur, Eve), (Catherine, Frank)]...

  Couvre 0 negatifs

  Gain FOIL : 3,234

5. Résolution inverse (bottom-up)

À l’inverse de FOIL (top-down), la résolution inverse part des faits et généralise. Deux opérateurs fondateurs (Muggleton) :

• Opérateur V (absorption) : si un littéral du corps d’une clause unifie avec un fait du background (nié), on retire ce littéral — il est « absorbé ».
• Opérateur W (identification) : on combine deux clauses en résolvant un littéral commun, produisant une clause plus générale.

#nullable enable
// Cellule 5 — Operateurs V (absorption) et W (identification)
public static HornClause? ApplyVOperator(HornClause clause, Literal backgroundFact)
{
    // backgroundFact est vu comme un fait positif ; on tente d'unifier (en l'inversant)
    // un littéral du corps avec le fait nie.
    for (int i = 0; i < clause.Body.Count; i++)
    {
        var bodyLit = clause.Body[i];
        var negBg = backgroundFact.WithNegated(!backgroundFact.Negated);
        var subst = Unify(bodyLit, negBg, new Dictionary<string,string>());
        if (subst is not null)
        {
            var newBody = new List<Literal>();
            for (int j = 0; j < clause.Body.Count; j++)
            {
                if (j == i) continue;
                newBody.Add(ApplySubst(clause.Body[j], subst));
            }
            var newHead = ApplySubst(clause.Head, subst);
            return new HornClause(newHead, newBody);
        }
    }
    return null;
}

public static Literal ApplySubst(Literal lit, Dictionary<string,string> subst)
    => lit.WithArgs(lit.Args.Select(a => subst.GetValueOrDefault(a, a)).ToArray());

public static List<HornClause> ApplyWOperator(HornClause c1, HornClause c2)
{
    var results = new List<HornClause>();
    // Litteraux de c1 (tete + corps) et c2 (tete + corps)
    var l1 = new List<Literal>{ c1.Head }; l1.AddRange(c1.Body);
    var l2 = new List<Literal>{ c2.Head }; l2.AddRange(c2.Body);
    for (int i = 0; i < l1.Count; i++)
    {
        for (int j = 0; j < l2.Count; j++)
        {
            var lit1 = l1[i]; var lit2 = l2[j];
            // Inverser le signe de lit1 pour la resolution
            var subst = Unify(lit1.WithNegated(!lit1.Negated), lit2, new Dictionary<string,string>());
            if (subst is null) continue;
            // Construire la clause resultante (retirer lit1 de c1 et lit2 de c2 par INDEX)
            var remaining = new List<Literal>();
            for (int k = 0; k < l1.Count; k++) if (k != i) remaining.Add(l1[k]);
            for (int k = 0; k < l2.Count; k++) if (k != j) remaining.Add(l2[k]);
            var newLits = remaining.Select(l => ApplySubst(l, subst)).ToList();
            var posLits = newLits.Where(l => !l.Negated).ToList();
            var negLits = newLits.Where(l => l.Negated).ToList();
            if (posLits.Count >= 1)
            {
                var body = negLits.Select(l => new Literal(l.Predicate, l.Args, false)).ToList();
                results.Add(new HornClause(posLits[0], body));
            }
        }
    }
    return results;
}

"Resolution inverse (bottom-up) sur ancestor".Display();
new string('=', 55).Display();
"".Display();
"Etape 2 : Operateur V (absorption)".Display();
var cl = new HornClause(new Literal("ancestor", new[]{"Arthur","Diana"}),
    new List<Literal>{ new Literal("parent", new[]{"Arthur","Bob"}), new Literal("parent", new[]{"Bob","Diana"}) });
$"  Clause initiale : {cl}".Display();
var resultV = ApplyVOperator(cl, new Literal("parent", new[]{"x","y"}));
$"  Apres V-operator : {resultV}".Display();
"".Display();
"Etape 3 : Operateur W (identification)".Display();
var c1w = new HornClause(new Literal("ancestor", new[]{"Arthur","Diana"}),
    new List<Literal>{ new Literal("parent", new[]{"Arthur","Bob"}), new Literal("ancestor", new[]{"Bob","Diana"}) });
var c2w = new HornClause(new Literal("ancestor", new[]{"Bob","Diana"}),
    new List<Literal>{ new Literal("parent", new[]{"Bob","Diana"}) });
$"  Clause 1 : {c1w}".Display();
$"  Clause 2 : {c2w}".Display();
foreach (var r in ApplyWOperator(c1w, c2w))
    $"  W-operator result : {r}".Display();

Resolution inverse (bottom-up) sur ancestor

=======================================================

Etape 2 : Operateur V (absorption)

  Clause initiale : ancestor(Arthur, Diana) :- parent(Arthur, Bob), parent(Bob, Diana).

  Apres V-operator : ancestor(Arthur, Diana) :- parent(Bob, Diana).

Etape 3 : Operateur W (identification)

  Clause 1 : ancestor(Arthur, Diana) :- parent(Arthur, Bob), ancestor(Bob, Diana).

  Clause 2 : ancestor(Bob, Diana) :- parent(Bob, Diana).

  W-operator result : ancestor(Arthur, Diana).

6. FOIL pas-à-pas (covering séquentiel)

L’algorithme complet de FOIL en covering séquentiel : on apprend une clause, on retire les positifs couverts, on recommence jusqu’à couvrir tous les positifs. Chaque clause est construite en ajoutant itérativement le littéral de meilleur gain (parmi les candidats, incluant le littéral récursif ancestor(.,.)), jusqu’à ce qu’elle ne couvre plus aucun négatif (clause consistante).

Deux ingrédients rendent la récursion apprenable : (a) la couverture compte des exemples distincts ; (b) le littéral récursif est évalué contre l’extension connue de la cible (les positifs déjà connus).

#nullable enable
// Cellule 6 — FOIL covering sequentiel avec trace
public static (List<HornClause> rules, HashSet<(string X,string Y)> uncovered) FoilStepByStep(
    string targetPred, string[] targetArgs, string[] constants,
    HashSet<(string Pred,string[] Args)> background,
    HashSet<(string X,string Y)> positives, HashSet<(string X,string Y)> negatives,
    List<Literal> candidateLiterals, int maxRules = 4)
{
    // Extension de la cible pour evaluer les litteraux recursifs
    var bgRec = new HashSet<(string,string[])>(background);
    foreach (var p in positives) bgRec.Add((targetPred, new[]{ p.X, p.Y }));

    var learnedRules = new List<HornClause>();
    var remainingPos = new HashSet<(string,string)>(positives);
    int ruleNum = 0;
    var sb = new System.Text.StringBuilder();
    while (remainingPos.Count > 0 && ruleNum < maxRules)
    {
        ruleNum++;
        sb.AppendLine($"--- Regle {ruleNum} ---");
        sb.AppendLine($"Positifs restants : {remainingPos.Count}");
        var bestBody = new List<Literal>();
        var coveredPos = new HashSet<(string,string)>(remainingPos);
        var coveredNeg = new HashSet<(string,string)>(negatives);

        for (int depth = 0; depth < 4; depth++)
        {
            sb.AppendLine($"  Profondeur {depth} : Body = [{string.Join(", ", bestBody)}]  pos={coveredPos.Count} neg={coveredNeg.Count}");
            if (coveredNeg.Count == 0) { sb.AppendLine("    -> Clause consistante !"); break; }
            double bestGain = double.NegativeInfinity;
            Literal? bestLit = null;
            HashSet<(string,string)> bestCp = new(), bestCn = new();
            foreach (var cand in candidateLiterals)
            {
                var trialBody = new List<Literal>(bestBody) { cand };
                var (cp, cn) = CheckClauseCovers(trialBody, targetPred, targetArgs, constants, bgRec, remainingPos, negatives);
                double g = FoilGain(coveredPos.Count, coveredNeg.Count, cp.Count, cn.Count);
                if (g > bestGain) { bestGain = g; bestLit = cand; bestCp = cp; bestCn = cn; }
            }
            if (bestLit is not null && bestGain > 0)
            {
                sb.AppendLine($"    Meilleur litteral : {bestLit} (gain={bestGain:F3})");
                bestBody.Add(bestLit);
                coveredPos = bestCp; coveredNeg = bestCn;
            }
            else { sb.AppendLine("    Pas d'amelioration possible"); break; }
        }
        if (bestBody.Count > 0 && coveredPos.Count > 0 && coveredNeg.Count == 0)
        {
            var rule = new HornClause(new Literal(targetPred, targetArgs), bestBody);
            learnedRules.Add(rule);
            sb.AppendLine($"  Regle apprise : {rule}");
            remainingPos.ExceptWith(coveredPos);
        }
        else
        {
            sb.AppendLine($"  Aucune clause consistante pour les {remainingPos.Count} positifs restants : arret.");
            break;
        }
    }
    sb.ToString().Display();
    return (learnedRules, remainingPos);
}

var CANDIDATES = new List<Literal> {
    new Literal("parent", new[]{"x","y"}), new Literal("parent", new[]{"y","x"}),
    new Literal("parent", new[]{"x","z"}), new Literal("parent", new[]{"z","y"}),
    new Literal("parent", new[]{"z","x"}), new Literal("parent", new[]{"y","z"}),
    new Literal("ancestor", new[]{"z","y"}), new Literal("ancestor", new[]{"x","z"}),
};

var (rules, uncovered) = FoilStepByStep("ancestor", new[]{"x","y"}, CONSTANTS, BACKGROUND, POSITIVES, NEGATIVES, CANDIDATES);
"".Display();
new string('=', 55).Display();
"Regles apprises par FOIL :".Display();
foreach (var r in rules) $"  {r}".Display();
$"Positifs non couverts : {(uncovered.Count == 0 ? "aucun (couverture complete)" : string.Join(", ", uncovered.OrderBy(p=>p.X)))}".Display();

--- Regle 1 ---
Positifs restants : 9
  Profondeur 0 : Body = []  pos=9 neg=10
    Meilleur litteral : parent(x, y) (gain=5,390)
  Profondeur 1 : Body = [parent(x, y)]  pos=5 neg=0
    -> Clause consistante !
  Regle apprise : ancestor(x, y) :- parent(x, y).
--- Regle 2 ---
Positifs restants : 4
  Profondeur 0 : Body = []  pos=4 neg=10
    Meilleur litteral : parent(x, z) (gain=1,942)
  Profondeur 1 : Body = [parent(x, z)]  pos=4 neg=6
    Meilleur litteral : ancestor(z, y) (gain=5,288)
  Profondeur 2 : Body = [parent(x, z), ancestor(z, y)]  pos=4 neg=0
    -> Clause consistante !
  Regle apprise : ancestor(x, y) :- parent(x, z), ancestor(z, y).

=======================================================

Regles apprises par FOIL :

  ancestor(x, y) :- parent(x, y).

  ancestor(x, y) :- parent(x, z), ancestor(z, y).

Positifs non couverts : aucun (couverture complete)

7. ILP sur un mini Knowledge Graph

Au-delà des arbres généalogiques, l’ILP découvre des règles relationnelles sur des KG (triples sujet-prédicat-objet). On illustre trois motifs classiques : symétrie du mariage, transitivité de localisation, et co-résidence des époux.

// Cellule 7 — Regles ILP sur un mini Knowledge Graph
var KG = new HashSet<(string S, string P, string O)> {
    ("Alice","marriedTo","Bob"), ("Bob","marriedTo","Alice"),
    ("Alice","livesIn","Paris"), ("Bob","livesIn","Paris"),
    ("Paris","locatedIn","France"), ("Lyon","locatedIn","France"),
    ("Charlie","livesIn","Lyon"), ("Diana","livesIn","Paris"),
    ("Diana","marriedTo","Charlie"), ("Charlie","marriedTo","Diana"),
};

"Mini Knowledge Graph".Display();
new string('=', 50).Display();
foreach (var (s,p,o) in KG.OrderBy(t=>t.S)) $"  ({s}, {p}, {o})".Display();
"".Display();

// 1. Symetrie du mariage : marriedTo(X,Y) :- marriedTo(Y,X).
"1. Symetrie du mariage : marriedTo(X, Y) :- marriedTo(Y, X).".Display();
int countSym = 0;
foreach (var (s,p,o) in KG)
    if (p == "marriedTo" && KG.Contains((o,"marriedTo",s))) countSym++;
$"   Couples verifiant la symetrie : {countSym}".Display();
"".Display();

// 2. Transitivite de localisation : livesIn(X,Z) :- livesIn(X,Y), locatedIn(Y,Z).
"2. Transitivite : livesIn(X, Z) :- livesIn(X, Y), locatedIn(Y, Z).".Display();
int countTrans = 0;
foreach (var (s1,p1,o1) in KG) if (p1 == "livesIn")
    foreach (var (s2,p2,o2) in KG) if (p2 == "locatedIn" && s2 == o1)
    {
        countTrans++;
        bool explicit_ = KG.Contains((s1,"livesIn",o2));
        if (countTrans <= 5)
            $"   {s1} livesIn {o1}, {o1} locatedIn {o2} => {s1} livesIn {o2} [{(explicit_ ? "EXPLICITE" : "IMPLICITE (infere)")}]".Display();
    }
$"   Total inferences possibles : {countTrans}".Display();
"".Display();

// 3. Co-residence des epoux : livesIn(X,L) :- marriedTo(X,Y), livesIn(Y,L).
"3. Co-residence des epoux : livesIn(X, L) :- marriedTo(X, Y), livesIn(Y, L).".Display();
int countCore = 0;
foreach (var (s1,p1,o1) in KG) if (p1 == "marriedTo")
    foreach (var (s2,p2,o2) in KG) if (p2 == "livesIn" && s2 == o1)
    {
        countCore++;
        bool verifie = KG.Contains((s1,"livesIn",o2));
        if (countCore <= 5)
            $"   {s1} marriedTo {o1}, {o1} livesIn {o2} => {s1} livesIn {o2} [{(verifie ? "EXPLICITE" : "NON VERIFIE")}]".Display();
    }
$"   Total inferences : {countCore}".Display();

Mini Knowledge Graph

==================================================

  (Alice, marriedTo, Bob)

  (Alice, livesIn, Paris)

  (Bob, marriedTo, Alice)

  (Bob, livesIn, Paris)

  (Charlie, livesIn, Lyon)

  (Charlie, marriedTo, Diana)

  (Diana, livesIn, Paris)

  (Diana, marriedTo, Charlie)

  (Lyon, locatedIn, France)

  (Paris, locatedIn, France)

1. Symetrie du mariage : marriedTo(X, Y) :- marriedTo(Y, X).

   Couples verifiant la symetrie : 4

2. Transitivite : livesIn(X, Z) :- livesIn(X, Y), locatedIn(Y, Z).

   Alice livesIn Paris, Paris locatedIn France => Alice livesIn France [IMPLICITE (infere)]

   Bob livesIn Paris, Paris locatedIn France => Bob livesIn France [IMPLICITE (infere)]

   Charlie livesIn Lyon, Lyon locatedIn France => Charlie livesIn France [IMPLICITE (infere)]

   Diana livesIn Paris, Paris locatedIn France => Diana livesIn France [IMPLICITE (infere)]

   Total inferences possibles : 4

3. Co-residence des epoux : livesIn(X, L) :- marriedTo(X, Y), livesIn(Y, L).

   Alice marriedTo Bob, Bob livesIn Paris => Alice livesIn Paris [EXPLICITE]

   Bob marriedTo Alice, Alice livesIn Paris => Bob livesIn Paris [EXPLICITE]

   Diana marriedTo Charlie, Charlie livesIn Lyon => Diana livesIn Lyon [NON VERIFIE]

   Charlie marriedTo Diana, Diana livesIn Paris => Charlie livesIn Paris [NON VERIFIE]

   Total inferences : 4

8. Exercices

Trois extensions à compléter (stubs C.1). Le notebook s’exécute end-to-end même non complété.

Exercice 1 — Négation par échec (NAF)

L’échec par négation (Negation As Failure) : not p(X) est vrai si p(X) ne peut pas être prouvé. Étendre EvaluateLiteral pour gérer les littéraux niés dans le corps via NAF.

Indice : un littéral nié ~lit est vrai si la version positive lit n’est PAS dans le background (déjà géré), mais pour un littéral contenant des variables liées, vérifier qu’aucune instanciation ne le satisfait.

// Cellule 8 — Exercice 1 (a completer) : negation par echec etendue
// TODO etudiant : etendre EvaluateLiteral pour la NAF sur variables liees
// Etape 1 : si lit.Negated est faux, comportement actuel (fact in background).
// Etape 2 : si lit.Negated est vrai ET certaines args sont des variables libres,
//           verifier qu'AUCUNE instanciation des variables libres n'est dans le background.
public static bool EvaluateLiteralNAF(Literal lit, Dictionary<string,string> binding,
    HashSet<(string Pred, string[] Args)> background, string[] constants)
{
    // TODO etudiant
    return false;   // stub
}
display("Exercice 1 (negation par echec) : stub a completer.");

Exercice 1 (negation par echec) : stub a completer.

Exercice 2 — Gain FOIL alternatif (entropie de Shannon)

FOIL utilise \(p \cdot \log_2(\frac{p}{p+n})\) comme gain. Une variante classique est le gain d’information de Shannon : \(\text{Gain} = H(parent) - \frac{N_{child}}{N_{parent}} H(child)\) où \(H(S) = -\frac{p}{p+n}\log_2\frac{p}{p+n} - \frac{n}{p+n}\log_2\frac{n}{p+n}\). L’implémenter et comparer les littéraux choisis.

Indice : attention aux cas limites (p=0 ou n=0 → H=0 par convention). Comparer le littéral sélectionné à chaque profondeur avec FOIL classique.

// Cellule 9 — Exercice 2 (a completer) : gain d'information de Shannon
// TODO etudiant : implementer ShannonGain(oldPos, oldNeg, newPos, newNeg)
// Etape 1 : definir H(p, n) = entropie de Shannon (0 si p=0 ou n=0).
// Etape 2 : Gain = H(oldPos, oldNeg) - (newTotal/oldTotal) * H(newPos, newNeg).
// Etape 3 : relancer FoilStepByStep avec ce gain et comparer les regles.
public static double ShannonGain(int oldPos, int oldNeg, int newPos, int newNeg)
{
    // TODO etudiant
    return 0.0;   // stub
}
display("Exercice 2 (gain de Shannon) : stub a completer.");

Exercice 2 (gain de Shannon) : stub a completer.

Exercice 3 — Apprentissage de la règle de transitivité

Sur le mini-KG, apprendre la règle transitive livesIn(X, Z) :- livesIn(X, Y), locatedIn(Y, Z) par FOIL (sans l’écrire à la main). Définir positives = tous les (X, Z) inférés, negatives = contre-exemples, background = le KG, et lancer FoilStepByStep.

Indice : convertir le KG en background (predicat, args[2]), définir les positifs comme les paires (X, Z) où il existe une chaîne livesIn-locatedIn, les négatifs comme des paires au hasard non connectées.

// Cellule 10 — Exercice 3 (a completer) : apprendre la regle transitive livesIn
// TODO etudiant : definir positifs/negatifs/background et appeler FoilStepByStep
// Etape 1 : background = KG converti en HashSet<(string, string[])>.
// Etape 2 : positifs = paires (X,Z) avec une chaine livesIn(X,Y)+locatedIn(Y,Z).
// Etape 3 : negatifs = paires (X,Z) sans chaine (prendre un echantillon).
// Etape 4 : candidats = livesIn(x,y), locatedIn(y,z), livesIn(x,z) et orientations.
// Etape 5 : FoilStepByStep("livesInDeep", ...) et verifier la regle apprise.
public static void LearnTransitivityRule(HashSet<(string S,string P,string O)> kg, string[] constants)
{
    // TODO etudiant
}
display("Exercice 3 (apprentissage transitivite) : stub a completer.");

Exercice 3 (apprentissage transitivite) : stub a completer.

9. Pont vers le solveur SOTA : clingo (Process.Start)

Le twin Python apprend ancestor/2 via Popper, qui formule l’ILP comme un problème ASP (Answer Set Programming) résolu par clingo (Potassco). Le verdict INTRINSIC (#10406) qui fermait cette section est révoqué par l’arbitrage #10382 : clingo est un binaire invocable, et le pendant C# honnête est Process.Start sur le même exécutable (axe CLI de la checklist SOTA #10459) — pas une réimplémentation.

La cellule suivante génère le programme ASP du problème ancestor(X, Y) à partir : 1. des faits parent/2 (BACKGROUND, cellule 3) ; 2. des règles apprises par notre FOIL from-scratch (cellule 6) : ancestor(x,y) :- parent(x,y) + ancestor(x,y) :- parent(x,z), ancestor(z,y).

puis invoque clingo (--outf=2) et vérifie que les ancêtres dérivés correspondent exactement aux 9 POSITIVES, sans atteindre aucun des 10 NEGATIVES. C’est la validation croisée du moteur from-scratch par le moteur SOTA — le même patron que le pont Gambit/nashpy de la série GameTheory.

Verdict SOTA (#3801)

Verdict	Détail
SOTA-OK (pont)	clingo (Potassco) invoqué depuis C# via Process.Start (axe CLI). Axes binding : pas de NuGet .NET (1), pas de P/Invoke (2), CLI = le canal (3), pas d’IKVM (4), pas de PythonNet (5). Le from-scratch FOIL (cellules 1-7) est conservé : le pont est en plus, jamais à la place — FOIL = l’algorithme fondateur d’AIMA §19.5, clingo = le moteur que Popper utilise en interne.

// === Pont clingo (Process.Start) : le moteur SOTA derrière Popper, invoqué depuis C# ===
// Parite lib-vs-lib (#10382) : le twin Python apprend `ancestor/2` via Popper, qui formule
// l'ILP comme un probleme ASP resolu par clingo (Potassco). Verdict INTRINSIC #10406 est
// REVOQUE : clingo est un binaire invocable via Process.Start (axe CLI checklist SOTA).
// On lance le MEME moteur sur le programme appris par notre FOIL from-scratch et on verifie
// que les ancetres derives correspondent exactement aux POSITIVES (9) sans toucher aux NEGATIVES.
using System.Diagnostics;
using System.IO;
using System.Text.Json;

// --- 1. Resolution portable du binaire clingo (regle F : outil reel, pas un stub) ---
static string[] FindClingoCmd()
{
    // Binaire Potassco : clingo.exe sous Windows, clingo ailleurs
    var clingoName = OperatingSystem.IsWindows() ? "clingo.exe" : "clingo";
    var envDir = Environment.GetEnvironmentVariable("CLINGO_DIR");
    if (!string.IsNullOrEmpty(envDir))
    {
        var exe = Path.Combine(envDir, clingoName);
        if (File.Exists(exe)) return new[] { exe };
    }
    // Installation de la serie SymbolicAI (install_clingo.py, gitignore : binaire non committe)
    var repoClingo = Path.Combine(
        Environment.CurrentDirectory, "MyIA.AI.Notebooks", "SymbolicAI", "ext_tools", "clingo", clingoName);
    if (File.Exists(repoClingo)) return new[] { repoClingo };
    // Fallback : binding Python Potassco (meme moteur C++) : python -m clingo, puis python3 -m clingo
    foreach (var py in new[] { "python", "python3" })   // python3 : Linux et macOS sans alias `python`
    {
        try
        {
            var pi = new ProcessStartInfo(py, "-c \"import clingo; print(clingo.__version__)\"")
            { RedirectStandardOutput = true, RedirectStandardError = true, UseShellExecute = false, CreateNoWindow = true };
            var p = Process.Start(pi);
            p.StandardOutput.ReadToEnd(); p.WaitForExit(5000);
            if (p.ExitCode == 0) return new[] { py, "-m", "clingo" };
        }
        catch { }
    }
    throw new FileNotFoundException(
        "clingo introuvable. Installer le solveur ASP SOTA (Potassco) : " +
        "python -m pip install clingo  OU  MyIA.AI.Notebooks/SymbolicAI/scripts/install_clingo.py");
}

// --- 2. Traduction C# -> ASP (variables x/y/z en MAJUSCULES, constantes en minuscules) ---
static string AspAtom(Literal l) =>
    l.Predicate + "(" + string.Join(",", l.Args.Select(a => char.IsUpper(a[0]) ? a.ToLowerInvariant() : a.ToUpperInvariant())) + ")";

static string AspRule(HornClause c) =>
    c.Body.Count == 0 ? $"{AspAtom(c.Head)}." : $"{AspAtom(c.Head)} :- {string.Join(",", c.Body.Select(AspAtom))}.";

// --- 3. Generation du programme ASP + invocation clingo ---
string aspPath = Path.Combine(Path.GetTempPath(), $"sl4_ancestor_{Guid.NewGuid():N}.asp");
var aspLines = new List<string>();
foreach (var (pred, args) in BACKGROUND)
    aspLines.Add($"parent({args[0].ToLowerInvariant()},{args[1].ToLowerInvariant()}).");
foreach (var r in rules)   // regles apprises par FOIL (cellule 6)
    aspLines.Add(AspRule(r));
File.WriteAllText(aspPath, string.Join("\n", aspLines));

var cmd = FindClingoCmd();
var psi = new ProcessStartInfo(cmd[0])
{
    RedirectStandardOutput = true, RedirectStandardError = true,
    UseShellExecute = false, CreateNoWindow = true,
    WorkingDirectory = Path.GetDirectoryName(aspPath) ?? Path.GetTempPath(),
};
foreach (var a in cmd.Skip(1)) psi.ArgumentList.Add(a);
psi.ArgumentList.Add("--outf=2");
psi.ArgumentList.Add(Path.GetFileName(aspPath));

var proc = Process.Start(psi);
string stdout = proc.StandardOutput.ReadToEnd();
string stderr = proc.StandardError.ReadToEnd();
proc.WaitForExit();

// --- 4. Parse des answer sets (--outf=2) + extraction des atomes ancestor/2 ---
var derived = new HashSet<(string X, string Y)>();
if (proc.ExitCode == 0 && !string.IsNullOrWhiteSpace(stdout))
{
    using var doc = JsonDocument.Parse(stdout);
    var witnesses = doc.RootElement.GetProperty("Call")[0].GetProperty("Witnesses");
    foreach (var w in witnesses.EnumerateArray())
        foreach (var atom in w.GetProperty("Value").EnumerateArray())
        {
            string s = atom.GetString();
            if (s.StartsWith("ancestor("))
            {
                var inner = s.Substring("ancestor(".Length, s.Length - "ancestor(".Length - 1).Split(',');
                derived.Add((char.ToUpperInvariant(inner[0][0]) + inner[0].Substring(1),
                             char.ToUpperInvariant(inner[1][0]) + inner[1].Substring(1)));
            }
        }
}

"===== Pont clingo (Process.Start) =====".Display();
$"Programme ASP ({aspLines.Count} lignes) :".Display();
foreach (var l in aspLines) $"  {l}".Display();
$"Solveur : {cmd[0]} {string.Join(" ", cmd.Skip(1))}".Display();
"".Display();
$"Ancetres derives par clingo : {derived.Count}".Display();
foreach (var (x, y) in derived.OrderBy(d => d.X).ThenBy(d => d.Y)) $"  ancestor({x}, {y})".Display();
"".Display();
var posCovers = POSITIVES.Count(p => derived.Contains(p));
var negLeaks = NEGATIVES.Count(n => derived.Contains(n));
$"POSITIVES couverts : {posCovers}/{POSITIVES.Count}".Display();
$"NEGATIVES atteints  : {negLeaks}/{NEGATIVES.Count}".Display();
$"Verdict parite : {(posCovers == POSITIVES.Count && negLeaks == 0 ? "FOIL from-scratch == clingo (SOTA) sur ancestor/2" : "ECART - investiguer")}".Display();

===== Pont clingo (Process.Start) =====

Programme ASP (7 lignes) :

  parent(arthur,bob).

  parent(arthur,catherine).

  parent(bob,diana).

  parent(catherine,eve).

  parent(eve,frank).

  ancestor(X,Y) :- parent(X,Y).

  ancestor(X,Y) :- parent(X,Z),ancestor(Z,Y).

Solveur : python -m clingo

Ancetres derives par clingo : 9

  ancestor(Arthur, Bob)

  ancestor(Arthur, Catherine)

  ancestor(Arthur, Diana)

  ancestor(Arthur, Eve)

  ancestor(Arthur, Frank)

  ancestor(Bob, Diana)

  ancestor(Catherine, Eve)

  ancestor(Catherine, Frank)

  ancestor(Eve, Frank)

POSITIVES couverts : 9/9

NEGATIVES atteints  : 0/10

Verdict parite : FOIL from-scratch == clingo (SOTA) sur ancestor/2

Lecture du résultat : FOIL from-scratch ≡ clingo (SOTA)

Les deux clauses apprises par le covering séquentiel de la cellule 6 sont rejouées telles quelles par le solveur ASP : ancestor(X,Y) :- parent(X,Y) (base) + ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y) (récursion). clingo les dérive par résolution — l’exacte mécanique que la cellule 5 reproduit opérateur V/W — et retrouve les 9 couples du problème, dont les transitifs (Arthur→Diana, Arthur→Eve, Arthur→Frank, Catherine→Frank). Aucun des 10 couples négatifs (remontées de graphe) n’est dérivé : le programme est correct au sens ILP (couvre tous les positifs, n’atteint aucun négatif).

Ce pont ferme l’asymétrie de la paire : le twin Python et ce twin C# invoquent le même moteur de recherche — la différence résiduelle est l’orchestrateur (Popper explore l’espace des programmes, ici on valide le programme trouvé par FOIL). Le parity_level de la paire passe de surface à native-both (les deux jumeaux référencent un moteur externe).

10. Résumé

Ce twin C# a reconstruit from-scratch (BCL .NET 9, 0 NuGet) le moteur de la programmation logique inductive :

1. Clauses Horn + unification : Literal/HornClause, UnifyVar/UnifyTerm/Unify (substitution θ, résolution par signes opposés).
2. FOIL top-down : EvaluateLiteral, CheckClauseCovers (énumération des substitutions + dédoublonnage sur les exemples), FoilGain (Quinlan \(p\log_2\frac{p}{p+n}\)).
3. Résolution inverse bottom-up : opérateurs V (absorption) et W (identification).
4. Covering séquentiel avec littéral récursif : redécouverte de ancestor(x,y) :- parent(x,y) et ancestor(x,y) :- parent(x,z), ancestor(z,y).
5. Mini-KG : symétrie, transitivité, co-résidence.

Leçon clé

L’ILP est le pont entre apprentissage et logique : il produit des règles compréhensibles (clauses Horn), à l’inverse des modèles boîte-noire. FOIL (top-down, gain d’information) et la résolution inverse (bottom-up, V/W) en sont les deux piliers algorithmiques. La complétude de recherche d’un outil SOTA comme Popper (ASP) n’est pas atteignable en .NET pur — d’où le verdict INTRINSIC, documenté honnêtement.

---

Marathon #4956 — twin C# .NET ⇄ Python. 1er twin SymbolicLearning po-2023. Suite logique : SL-3 (RelevanceLearning) et SL-5 (InverseResolution, déjà twinné). Voir #4956, #3801. Revue souhaitée : ai-01, po-2024, po-2025.