Aricie B2 (Logic) — tranche 1 : noyau propositionnel (PL) vers MyIA.AI.Shared/Search/Logic/Propositional/ #23584

Grain: DEEP/research-code — lane myia-ai-01:CoursIA-2 — prev: MED/tooling #23117

Part of #7265 — tranche d'execution du volet B2 (port Aricie vers MyIA.AI.Shared), ouverte sur le scoping #21909 (« Toute tranche d'execution ouverte par la suite cite cette issue »).

Ce que porte cette tranche

Le noyau propositionnel de Logic.cs du patrimoine Aricie (Libraries/AI/Logic.cs, 401 lignes), porte en C# nu dans MyIA.AI.Shared/Search/Logic/Propositional/, sur la surface d'API que le wrapper Aricie expose :

• PLKbInfo -> base de connaissances propositionnelle (sentences) ;
• PLKbInferProcedureInfo -> une procedure d'inference au choix, appliquee a une base et a un predicat.

Les procedures couvertes : TTEntails, Resolve, DPLLEntails, DPLLSatisfiable, WalkSatKb, WalkSatPredicate.

Ce qui reste hors de cette tranche (et pourquoi)

• FOL (FolKbInfo, FolDomainInfo, les cinq procedures FOL) : c'est le point de decision n°1 de Aricie #7265 - Scoping du reste B2 : Logic.cs / Probability.cs / Neural.cs (Libraries/AI) #21909 (Z3.Linq comme solveur, ou non-cible explicite). La decision du mainteneur conditionne le moteur ; la tranche s'arrete avant.
• Probability.cs (point de decision n°2) et Neural.cs (point de decision n°3, non-cible recommandee en l'etat).
• PLFCEntails : la semantique exacte de cette procedure n'est pas etablie — le comportement derriere le wrapper est dans aima-core.dll, un binaire qui n'a pas ete rejoue. Elle est reportee, pas approximee.

Acceptance

• MyIA.AI.Shared/Search/Logic/Propositional/ existe : parseur PL, base de connaissances, et les six procedures listees ci-dessus.
• Temoins xunit dans MyIA.AI.Shared.Tests/Search/Logic/ : exemple AIMA ch.7 (base {~A | B, A} entailt B), satisfiabilite DPLL, formule insatisfiable (temoignage des trois clauses de AIMA), et un cas de discrimination mesuree entre procedures (comptage de lignes de table de verite, de noeuds DPLL et de flips WalkSAT sur la meme instance) — la tranche doit rendre les procedures falsifiables entre elles, pas seulement correctes.
• dotnet test MyIA.AI.Shared.Tests vert sur la suite complete (pas seulement les nouveaux tests).
• MyIA.AI.Shared/README.md : ligne de tracabilite de la tranche (l'index de la pompe).
• Le body de la PR repond aux cinq questions de la regle organ-first-implementation (organe natif existant, module invocable, temoin negatif, verification independante).

Portee du non-verifie

Le comportement d'aima-core.dll derriere chaque wrapper *Info n'a pas ete rejoue (binaire non decompile) : la portee ci-dessus est deduitee de la surface publique des wrappers et de la semantique du chapitre 7 d'AIMA.