Ce notebook d’initialisation verifie que l’environnement d’exécution formel est operationnel : Python, la passerelle JPype vers la JVM, le JDK 17 portable et les jars de TweetyProject. Il se termine par un smoke test qui interroge le vrai solveur propositionnel Tweety (un modus ponens meteorologique). C’est la porte d’entree de la serie : une fois ce rung valide, les rungs 1 a 4 s’appuient sur un socle formel reel.
Note anti-theatre : cette serie refuse le mode degrade. Si la JVM ou Tweety est absent, le notebook echoue bruyamment (le smoke test de la section 5 ne peut pas charger les classes Tweety via JPype) plutot que de simuler un raisonnement formel. Un solveur formel simule par un LLM n’est PAS un solveur formel (mandat EPITA #2137). Cette cellule d’init est donc le verrou qui garantit que les rungs suivants tournent sur du vrai.
1. Pourquoi un rung d’initialisation
Les notebooks précédents (1-informal, 3-orchestration, 4-capstone) restent deliberement déterministes et pur Python : ils n’ont pas besoin de la JVM pour s’executer. Le rung 2-formal, lui, invoque le vrai solveur Tweety (logiques propositionnelle, du premier ordre, modale, argumentation de Dung) via un pont Python-Java (JPype). Ce rung 0-init est le detecteur de fumee de ce socle Java : il verifie chaque composant et produit un temoin d’exécution (JVM_OK = True) que les notebooks suivants peuvent reutiliser.
Ce que ce rung fait
Verifie que jpype est importable (passerelle Python-Java).
Localise le dossier Tweety/ (JDK 17 portable + les jars) via la shim argumentation_lib, fail-loud s’il manque.
Demarre la JVM via la shim argumentation_lib.initialize_jvm(), fail-loud si elle ne s’amorce pas.
Execute un smoke test : un modus ponens meteorologique resolu par le vrai SimplePlReasoner de Tweety.
Recapitule l’etat de l’environnement dans une checklist.
Ce que ce rung ne fait pas
Pas d’appel LLM ni de semantic_kernel (le legacy 0-init_agent.ipynb couvrait la configuration LLM/OpenAI ; ce compact se concentre sur le socle formel).
Pas d’extraction informelle ni de detection de sophismes (rung 1).
2. Verification Python : la passerelle JPype
jpype est la passerelle qui permet a Python d’invoquer des classes Java (Tweety est une bibliotheque JVM). Sans elle, aucun pont vers la JVM n’est possible.
import sysprint(f"Python : {sys.version.split()[0]}")try:import jpypeprint(f"JPype : {jpype.__version__} (passerelle Python-Java OK)") JPYPE_OK =TrueexceptImportErroras e:print(f"JPype ABSENT : {e}")print("Installez avec : pip install jpype1") JPYPE_OK =False# Aucun guard fatal dans la cellule (regle C.1 : pas de raise). Si JPype est# absent, l'amorcage de la JVM via la shim a la section 4 ne demarrera pas et le# smoke test de la section 5 echouera alors bruyamment (impossible de charger les# classes Tweety). Le mode degrade (simulation LLM d'un solveur formel) reste# interdit par construction (anti-theatre, mandat EPITA #2137).
init_tweety() cherche les dossiers libs/ (les jars Tweety – le decompte depend de la machine, cf sortie de la cellule de localisation) et jdk-17-portable/ (le JDK Zulu 17) relativement au repertoire de travail courant. On marche donc vers le haut depuis le cwd jusqu’a trouver Tweety/libs. Si rien n’est trouve, echec bruyant : le mode degrade est interdit.
# Localisation du dossier Tweety via la shim argumentation_lib. La robustesse# cwd (resolution __file__-relative, AUCUN walk manuel) est portee par la shim# (_paths.py), comme aux rungs 1/2/3/4 -- aucun guard de path ni raise dans la# cellule (regle C.1).from argumentation_lib._paths import SYMBOLIC_AI_DIRTWEETY_DIR = SYMBOLIC_AI_DIR /"Tweety"libs_dir = TWEETY_DIR /"libs"jdk_root = TWEETY_DIR /"jdk-17-portable"jars =sorted(libs_dir.glob("*.jar"))print(f"Dossier Tweety resolu via la shim : {TWEETY_DIR}")print(f"Jars Tweety trouves : {len(jars)}")print(f"JDK portable present : {jdk_root.is_dir()}")# Aucun raise (regle C.1) : si les composants manquent, l'amorcage JVM de la# section 4 retournera False et le smoke test de la section 5 echouera# bruyamment. Le mode degrade (simulation) reste interdit (anti-theatre #2137).
Dossier Tweety resolu via la shim : <repo>\MyIA.AI.Notebooks\SymbolicAI\Tweety
Jars Tweety trouves : 42
JDK portable present : True
4. Demarrage de la JVM via init_tweety()
init_tweety() configure JAVA_HOME sur le JDK Zulu 17, construit le classpath avec les jars du dossier libs/ (decompte dependant de la machine, cf sortie de la cellule de localisation), et amorce la JVM via JPype. L’appel se fait depuis le dossier Tweety (il resout les chemins relativement au cwd). Echec bruyant si la JVM ne demarre pas.
import jpype# Amorcage de la JVM via la shim argumentation_lib. La shim resout le dossier# Tweety (cwd-indep), stage sys.path pour rendre Tweety.tweety_init importable,# chdir dans le dossier Tweety, puis appelle init_tweety() -- elle encapsule# toute la configuration manuelle (classpath, JAVA_HOME, jars). Aucun appel# direct a tweety_init, aucun guard de path/raise dans la cellule (regle C.1),# comme au rung 2-formal (#3857).from argumentation_lib import initialize_jvmJVM_OK = initialize_jvm(verbose=True)print(f"")print(f"JVM operationnelle : {jpype.isJVMStarted()}")print(f"Classpath Tweety charge depuis : {TWEETY_DIR /'libs'}")print(f"Amorcage shim reussi : {JVM_OK}")
5. Smoke test : un modus ponens meteorologique resolu par le vrai Tweety
Pour prouver que la JVM ne tourne pas a vide, on interroge le vrai SimplePlReasoner de Tweety sur un modus ponens trivial : « s’il pleut, le sol est mouille ; il pleut ; donc le sol est mouille ». Le solveur doit repondre True pour wet et False pour !wet. C’est le temoin d’exécution : si ce smoke test passe, le socle formel est operationnel pour les rungs suivants.
Pattern identique au rung 2-formal, recycle ici comme preuve que l’environnement est pret.
import jpypeJClass = jpype.JClass# Classes Tweety pour la logique propositionnelle.PlParser = JClass("org.tweetyproject.logics.pl.parser.PlParser")SimplePlReasoner = JClass("org.tweetyproject.logics.pl.reasoner.SimplePlReasoner")PlBeliefSet = JClass("org.tweetyproject.logics.pl.syntax.PlBeliefSet")parser = PlParser()bs = PlBeliefSet()bs.add(parser.parseFormula("rain => wet")) # S'il pleut, alors le sol est mouille.bs.add(parser.parseFormula("rain")) # Il pleut.reasoner = SimplePlReasoner()entails_wet =bool(reasoner.query(bs, parser.parseFormula("wet")))entails_not_wet =bool(reasoner.query(bs, parser.parseFormula("!wet")))print("--- Smoke test Tweety : modus ponens meteorologique ---")print(f"Belief set : {{rain => wet, rain}}")print(f" wet entailed ? {entails_wet} (attendu : True)")print(f" !wet entailed ? {entails_not_wet} (attendu : False)")# Le smoke test est le temoin : si ces deux valeurs sont correctes, la JVM Tweety# resout reellement la logique propositionnelle (pas une simulation).SMOKE_OK = entails_wet andnot entails_not_wet# Aucun raise (regle C.1) : SMOKE_OK=False signale un probleme de coherence des# jars sans interrompre le notebook. Si la JVM etait absente (section 4), cette# cellule aurait deja echoue bruyamment ci-dessus : jpype.JClass ne peut pas# charger les classes Tweety sans JVM demarree -- le mode degrade reste interdit.print(f"")print(f"SMOKE_OK = {SMOKE_OK} : socle formel operationnel pour les rungs suivants.")
--- Smoke test Tweety : modus ponens meteorologique ---
Belief set : {rain => wet, rain}
wet entailed ? True (attendu : True)
!wet entailed ? False (attendu : False)
SMOKE_OK = True : socle formel operationnel pour les rungs suivants.
6. Recapitulatif de l’environnement
Composant
Rôle
Etat
Python + JPype
Passerelle Python-Java
OK
JDK (Zulu 17 portable, sinon JAVA_HOME)
Machine virtuelle Java
OK via la sonde JVM ci-dessus
Jars Tweety
Solveurs (PL, FOL, modale, Dung)
OK
argumentation_lib.initialize_jvm()
Amorcage JVM + classpath (via la shim)
OK
Smoke test PL
Modus ponens resolu
OK
L’environnement formel est pret. Les rungs suivants peuvent maintenant invoquer le vrai solveur Tweety :
1-informal : detection de sophismes (pur Python, n’a pas besoin de la JVM mais s’inscrit dans la même serie).
2-formal : verifications PL / FOL / modale / Dung avec le vrai Tweety (reutilise ce socle).
4-capstone : capstone d’integration avec value-gates.
Le mode degrade est interdit
Si un jour ce notebook echoue au smoke test (les classes Tweety sont introuvables via JPype, signe que la JVM ou les jars sont absents), ne contournez pas en simulant le solveur avec un LLM. La valeur pedagogique de la serie repose sur le fait que le formel est REEL. Reinstallez le JDK portable et les jars, puis re-executez ce notebook jusqu’a SMOKE_OK = True.
Exercice (optionnel) : etendre le smoke test a la logique du premier ordre
Le smoke test ci-dessus couvre la logique propositionnelle (PL). Etendez-le a un syllogisme en logique du premier ordre (FOL) avec le vrai SimpleFolReasoner : par exemple « Tous les oiseaux volent ; Tweety est un oiseau ; donc Tweety vole ». Reutilisez le pattern FOL du rung 2-formal (pre-declaration de signature obligatoire : parser.setSignature(sig)). Ajoutez un flag FOL_SMOKE_OK et verifiez qu’il vaut True.
# Exercice optionnel -- a completer# TODO etudiant : smoke test FOL avec SimpleFolReasoner (syllogisme oiseau/vole).# Indice : pre-declarer la signature (Sort, Constant, Predicate) AVANT parser.setSignature(sig).# Etape 1 : construire FolSignature + FolBeliefSet.# Etape 2 : parser les formules FOL ("forall X: ...").# Etape 3 : query Tweety et positionner FOL_SMOKE_OK.result =None# TODO etudiantprint("Exercice optionnel a completer : smoke test FOL (syllogisme oiseau/vole) avec SimpleFolReasoner")
Exercice optionnel a completer : smoke test FOL (syllogisme oiseau/vole) avec SimpleFolReasoner