Ce notebook configure l’environnement pour la série de notebooks TweetyProject qui explore la bibliothèque Java TweetyProject pour l’intelligence artificielle symbolique.
IMPORTANT: Ce notebook Tweety-1-Setup configure uniquement l’environnement. Les exemples de logiques et d’argumentation se trouvent dans les notebooks suivants de la série.
Cette section couvre la mise en place de l’environnement nécessaire pour exécuter les exemples de ce notebook.
1.2 Pré-requis
Python 3.x : Assurez-vous d’avoir une installation Python fonctionnelle (testé avec 3.10+).
Java Development Kit (JDK) : JPype nécessite un JDK (version 11 ou supérieure recommandée) pour démarrer la JVM.
Vérifiez votre installation avec java -version dans un terminal.
Assurez-vous que la variable d’environnement JAVA_HOME pointe vers le répertoire racine de votre installation JDK (par exemple, /usr/lib/jvm/java-17-openjdk-amd64 sur Linux, C:\Program Files\Java\jdk-17 sur Windows).
Si JAVA_HOME n’est pas définie, le script de démarrage de la JVM (section 1.6) essaiera de trouver un JDK automatiquement, mais il est préférable de la définir explicitement.
(Optionnel) Outils Externes : Pour certaines fonctionnalités avancées (voir section 1.5), vous devrez installer des outils spécifiques et configurer leurs chemins d’accès plus loin dans le notebook.
(Optionnel) Graphviz: Pour visualiser certains graphes d’argumentation (non implémenté dans ce tutoriel mais possible).
1.3 Installation des Packages Python
Nous utilisons jpype1 pour le pont Java-Python. Les autres packages (requests, tqdm) sont des utilitaires pour le téléchargement des JARs.
# Vérification/Installation des packages Python nécessairesimport importlibimport sysimport subprocess# Le package s'appelle 'jpype1' sur PyPI, mais on importe 'jpype'# z3 s'importe comme 'z3' mais s'installe comme 'z3-solver'# pysat s'importe comme 'pysat' mais s'installe comme 'python-sat'packages_to_check = {'jpype': 'jpype1','requests': 'requests','tqdm': 'tqdm','clingo': 'clingo','z3': 'z3-solver', # Pour MARCO (MUS enumeration) et SMT solving'pysat': 'python-sat'# Pour MaxSAT (RC2) et solveurs SAT modernes (CaDiCaL)}packages_to_install = []all_found =Trueprint("--- Vérification des packages Python requis ---")for import_name, install_name in packages_to_check.items():try: importlib.import_module(import_name)print(f"✔️ {import_name} trouvé.")exceptImportError:print(f"⚠️ {import_name} manquant (package: {install_name}).") packages_to_install.append(install_name) all_found =Falseif packages_to_install:print(f"\nTentative d'installation des packages manquants: {', '.join(packages_to_install)}...")try:# Utiliser -q pour une sortie moins verbeuse, retirer si le debug est nécessaire subprocess.check_call([sys.executable, "-m", "pip", "install", "-q"] + packages_to_install)print(f"✅ Packages {', '.join(packages_to_install)} installés.")print("\n‼️ IMPORTANT : Vous devez probablement REDÉMARRER LE NOYAU (Kernel -> Restart Kernel) pour que les nouveaux packages soient pris en compte.")# Marquer comme non trouvés pour l'instant, car le noyau doit redémarrer all_found =FalseexceptExceptionas e:print(f"❌ Échec de l'installation automatique : {e}")print(f" Veuillez installer manuellement : pip install {' '.join(packages_to_install)}") all_found =False# Échec -> pas trouvéif all_found:print("\n✔️ Tous les packages Python requis sont présents.")# Importations pour vérifier après redémarrage potentiel (ne lèvera pas d'erreur ici)try:import jpypeimport requestsimport tqdmexceptImportError:ifnot packages_to_install: # Si on n'a pas essayé d'installer, c'est une autre erreurprint("\n⚠️ Erreur d'import inattendue. Vérifiez votre environnement Python.")# Si on a installé, le message d'erreur est déjà affiché.pass
--- Vérification des packages Python requis ---
⚠️ jpype manquant (package: jpype1).
✔️ requests trouvé.
✔️ tqdm trouvé.
⚠️ clingo manquant (package: clingo).
⚠️ z3 manquant (package: z3-solver).
⚠️ pysat manquant (package: python-sat).
Tentative d'installation des packages manquants: jpype1, clingo, z3-solver, python-sat...
✅ Packages jpype1, clingo, z3-solver, python-sat installés.
‼️ IMPORTANT : Vous devez probablement REDÉMARRER LE NOYAU (Kernel -> Restart Kernel) pour que les nouveaux packages soient pris en compte.
1.4 Téléchargement des JARs Tweety et Dépendances
TweetyProject est une collection de bibliothèques Java distribuées sous forme de fichiers JAR. Pour utiliser Tweety avec JPype, nous devons télécharger ces JARs et les rendre accessibles à la JVM.
Le script suivant va : 1. Créer un sous-dossier libs/ s’il n’existe pas. 2. Vérifier si l’URL de base pour la version spécifiée de Tweety (TWEETY_VERSION) est accessible. 3. Télécharger (ou vérifier la présence) du JAR principaltweety-full-...-with-dependencies.jar. Celui-ci contient le noyau de Tweety et de nombreuses dépendances courantes. 4. Télécharger (ou vérifier la présence) des JARs spécifiques aux modules utilisés dans ce notebook (argumentation, logiques spécifiques, etc.). La liste REQUIRED_MODULES définit les modules nécessaires.
Note : Le téléchargement peut prendre quelques minutes lors de la première exécution. Assurez-vous que tous les JARs nécessaires sont bien présents dans le dossier libs/ avant de démarrer la JVM, car des JARs manquants causeront des erreurs d’import plus loin.
Interprétation de la vérification des packages
Résultat attendu : Si tous les packages sont déjà installés, vous verrez un message confirmant leur présence. Si des packages manquent, le script tente une installation automatique.
Note importante : Si des packages ont été installés automatiquement, vous devez redémarrer le kernel Jupyter pour que les imports fonctionnent correctement. La cellule affiche alors un avertissement explicite.
Packages requis et leur rôle :
Package
Rôle dans Tweety
jpype1
Pont Python-Java pour interfacer avec TweetyProject
requests
Téléchargement des JARs depuis tweetyproject.org
tqdm
Barres de progression pour les téléchargements
clingo
Solveur ASP (Answer Set Programming)
z3-solver
SMT solver pour MARCO (énumération MUS)
python-sat
Solveurs SAT modernes (CaDiCaL, Glucose, RC2 MaxSAT)
Prochaine étape : Téléchargement des bibliothèques Java de TweetyProject.
# --- Telechargement des JARs TweetyProject ---print("\n"+"="*70)print("TELECHARGEMENT DES JARS TWEETYPROJECT")print("="*70)# Le telechargement utilise maintenant le script helper scripts/download_tweety_tools.py# Ce script centralise tous les telechargements et peut etre reutilise hors des notebooks.import subprocessimport sysimport pathlibscript_path = pathlib.Path("scripts/download_tweety_tools.py")ifnot script_path.exists():print(f"ERREUR: Script non trouve: {script_path}")print("Assurez-vous d'executer ce notebook depuis le repertoire Tweety/")else:print(f"Execution du script: {script_path}") result = subprocess.run( [sys.executable, str(script_path), "--jars"], capture_output=True, text=True, encoding="utf-8", errors="replace" )print(result.stdout)if result.returncode !=0:print("ERREUR:", result.stderr)else:print("\nOK Telechargement des JARs termine avec succes!")# Verifier que les JARs ont ete telechargesLIB_DIR = pathlib.Path("libs")if LIB_DIR.exists(): jars =list(LIB_DIR.glob("*.jar"))print(f"\nJARs presents dans libs/: {len(jars)}")if jars:print("Premiers JARs:")for jar insorted(jars)[:5]:print(f" - {jar.name}")
Certaines fonctionnalités avancées de Tweety s’appuient sur des outils externes (solveurs SAT/MaxSAT, prouveurs FOL/ML, énumérateurs MUS, solveurs ASP). Pour utiliser ces fonctionnalités, vous devez :
Installer l’outil externe séparément en suivant les instructions de son site web.
Indiquer le chemin d’accès à l’exécutable de l’outil dans la cellule de code ci-dessous.
Outils potentiellement utilisés dans ce notebook :
Solveurs SAT externes (pour logics.pl.sat.CmdLineSatSolver - Section 2.1.3) :
Lingeling, CaDiCaL, Kissat, MiniSat, Glucose, etc. (prennent souvent le format DIMACS)
PicoSAT, Lingeling, MiniSat (fournis avec Tweety pour certaines plateformes, voir libs/)
Instructions : * Modifiez les variables *_PATH dans la cellule suivante avec les chemins corrects sur votre système. * Si un outil n’est pas installé ou si vous ne souhaitez pas l’utiliser, laissez le chemin vide ("") ou commentez la ligne correspondante. Le notebook essaiera d’utiliser des alternatives internes (plus lentes) ou sautera les sections concernées. * Sous Windows, n’oubliez pas l’extension .exe et utilisez des anti-slashs (\\) ou des slashs (/) pour les chemins.
Interprétation du téléchargement des fichiers
Résultat obtenu : Le script affiche un résumé indiquant combien de fichiers ont été téléchargés, combien étaient déjà présents, et s’il y a eu des échecs.
Structure des fichiers de données :
Les fichiers téléchargés sont organisés par type de logique/argumentation :
Catégorie
Exemples
Format
DeLP
birds.txt, nixon.txt
Règles défaisables
ABA
example1.aba, example2.aba
Assumptions et règles
ASPIC+
ex1.aspic, ex5_fol.aspic
Arguments strictes/défaisables
Logiques
*.proplogic, *.fologic, *.mlogic
Formules logiques
Argumentation
*.tgf, *.apx, adf_example.txt
Frameworks
Conseil : Explorez le dossier resources/ pour voir les exemples disponibles. Ces fichiers seront utilisés dans les notebooks suivants de la série.
# --- Configuration de base pour les outils externes ---import osimport pathlibimport platformimport shutilimport subprocessimport urllib.requestimport zipfileimport stat# Repertoire pour les outils externesEXT_TOOLS_DIR = pathlib.Path("ext_tools")EXT_TOOLS_DIR.mkdir(exist_ok=True)# Repertoire pour les bibliotheques natives SAT (pour ADF)NATIVE_LIBS_DIR = pathlib.Path("../libs/native")ifnot NATIVE_LIBS_DIR.exists():for alt in [pathlib.Path("libs/native"), pathlib.Path("../../libs/native")]:if alt.exists(): NATIVE_LIBS_DIR = altbreak# Dictionnaire pour stocker les chemins des outils externesEXTERNAL_TOOLS = {"SAT_SOLVER": "","SAT_SOLVER_PYTHON": "", # Nouveau: wrapper Python avec CaDiCaL"EPROVER": "","MARCO": "","OPEN_WBO": "","CLINGO": "","SPASS": ""}def get_tool_path(tool_name):"""Retourne le chemin valide d'un outil ou None.""" path_str = EXTERNAL_TOOLS.get(tool_name, "")ifnot path_str: returnNoneif shutil.which(path_str):return path_str path_obj = pathlib.Path(path_str)if path_obj.is_file() and os.access(path_obj, os.R_OK):returnstr(path_obj.resolve())returnNonesystem = platform.system()print(f"Configuration des outils externes pour {system}")print(f"Repertoire ext_tools: {EXT_TOOLS_DIR.resolve()}")print(f"Repertoire libs/native: {NATIVE_LIBS_DIR.resolve() if NATIVE_LIBS_DIR.exists() else'Non trouve'}")
Configuration des outils externes pour Windows
Repertoire ext_tools: <repo>MyIA.AI.Notebooks\SymbolicAI\Tweety\ext_tools
Repertoire libs/native: <repo>MyIA.AI.Notebooks\SymbolicAI\libs\native
1.5.1 Clingo - Solveur ASP (Answer Set Programming)
Clingo est le solveur ASP de reference du projet Potassco. Il combine le grounder gringo et le solveur clasp.
Utilisation dans Tweety : - lp.asp.reasoner.ClingoSolver : Raisonnement ASP - Support des programmes avec defauts et contraintes d’integrite
Installation : Si non present, telechargement automatique depuis GitHub.
# === Configuration de Clingo ===print("=== 1. Configuration de Clingo ===")clingo_dir = EXT_TOOLS_DIR /"clingo"clingo_dir.mkdir(exist_ok=True)clingo_exe = clingo_dir / ("clingo.exe"if system =="Windows"else"clingo")# Verifier si clingo est deja presentclingo_in_path = shutil.which("clingo") or shutil.which("clingo.exe")if clingo_in_path: EXTERNAL_TOOLS["CLINGO"] = clingo_in_pathprint(f" OK Clingo trouve dans PATH: {clingo_in_path}")elif clingo_exe.exists(): EXTERNAL_TOOLS["CLINGO"] =str(clingo_exe.resolve())print(f" OK Clingo deja present: {clingo_exe}")else:# Telecharger automatiquementprint(" Telechargement de Clingo...") clingo_version ="5.4.0"if system =="Windows": clingo_url =f"https://github.com/potassco/clingo/releases/download/v{clingo_version}/clingo-{clingo_version}-win64.zip" clingo_archive = clingo_dir /"clingo.zip"try: urllib.request.urlretrieve(clingo_url, clingo_archive)with zipfile.ZipFile(clingo_archive, 'r') as zip_ref: zip_ref.extractall(clingo_dir)for exe in clingo_dir.rglob("clingo.exe"): shutil.move(str(exe), str(clingo_exe)) EXTERNAL_TOOLS["CLINGO"] =str(clingo_exe.resolve())print(f" OK Clingo installe: {clingo_exe}")break clingo_archive.unlink(missing_ok=True)for d in clingo_dir.glob("clingo-*"):if d.is_dir(): shutil.rmtree(d, ignore_errors=True)exceptExceptionas e:print(f" Erreur telechargement Clingo: {e}")elif system =="Linux":import tarfile clingo_url =f"https://github.com/potassco/clingo/releases/download/v{clingo_version}/clingo-{clingo_version}-linux-x86_64.tar.gz" clingo_archive = clingo_dir /"clingo.tar.gz"try: urllib.request.urlretrieve(clingo_url, clingo_archive)with tarfile.open(clingo_archive, "r:gz") as tar: tar.extractall(path=clingo_dir)for exe in clingo_dir.rglob("clingo"):if exe.is_file(): shutil.move(str(exe), str(clingo_exe)) os.chmod(clingo_exe, stat.S_IRWXU | stat.S_IRGRP | stat.S_IXGRP) EXTERNAL_TOOLS["CLINGO"] =str(clingo_exe.resolve())print(f" OK Clingo installe: {clingo_exe}")break clingo_archive.unlink(missing_ok=True)exceptExceptionas e:print(f" Erreur installation Clingo: {e}")
=== 1. Configuration de Clingo ===
OK Clingo deja present: ext_tools\clingo\clingo.exe
1.5.2 SPASS - Prouveur de Logique Modale
SPASS est un prouveur automatique de theoremes pour la logique du premier ordre avec support pour la logique modale.
Utilisation dans Tweety : - logics.ml.reasoner.SPASSMlReasoner : Raisonnement en logique modale (Section 2.4)
Note : Sans SPASS, SimpleMlReasoner peut bloquer indefiniment. SPASS est donc fortement recommande pour les notebooks sur la logique modale.
# === Configuration de SPASS ===print("=== 2. Configuration de SPASS ===")spass_dir = EXT_TOOLS_DIR /"spass"spass_dir.mkdir(exist_ok=True)spass_exe = spass_dir / ("SPASS.exe"if system =="Windows"else"SPASS")# IMPORTANT: Le fichier spass30windows.exe sur le site SPASS est un INSTALLEUR,# pas un executable standalone. Il lance une interface d'installation a chaque appel.# => On ne telecharge PAS automatiquement sous Windows.spass_in_path = shutil.which("SPASS") or shutil.which("SPASS.exe")if spass_in_path: EXTERNAL_TOOLS["SPASS"] = spass_in_pathprint(f" OK SPASS trouve dans PATH: {spass_in_path}")elif spass_exe.exists():# Verifier que ce n'est pas l'installeur (taille > 1MB = probablement standalone) file_size = spass_exe.stat().st_sizeif file_size >1_000_000: # > 1MB = probablement l'installeurprint(f" WARN Le fichier {spass_exe} semble etre l'installeur SPASS.")print(f" Taille: {file_size/1024:.0f} KB (attendu ~200-500 KB pour standalone)")print(f" Supprimez-le et installez SPASS manuellement.")else: EXTERNAL_TOOLS["SPASS"] =str(spass_exe.resolve())print(f" OK SPASS deja present: {spass_exe}")else:if system =="Windows":# NE PAS telecharger automatiquement - le fichier est un installeur, pas un executableprint(" INFO SPASS non configure.")print(" Pour Windows, installez SPASS manuellement:")print(" 1. Telecharger depuis: https://www.spass-prover.org/download/binaries/")print(" 2. Choisir 'spass30windows.exe' et EXECUTER l'installeur")print(" 3. Copier SPASS.exe du repertoire d'installation vers:")print(f" {spass_dir}")print(" 4. Re-executer cette cellule")print("")print(" Note: SPASS est OPTIONNEL. La logique modale fonctionne sans raisonnement.")elif system =="Linux":import tarfile arch ="64"if platform.architecture()[0] =="64bit"else"32" spass_url =f"https://www.spass-prover.org/download/binaries/spass35pclinux{arch}.tgz" spass_archive = spass_dir /"spass.tgz"print(f" Telechargement de SPASS pour Linux ({arch}bit)...")try: urllib.request.urlretrieve(spass_url, spass_archive)with tarfile.open(spass_archive, "r:gz") as tar: tar.extractall(path=spass_dir) extracted = spass_dir /"SPASS"/"SPASS"if extracted.exists(): shutil.move(str(extracted), str(spass_exe)) os.chmod(spass_exe, stat.S_IRWXU | stat.S_IRGRP | stat.S_IXGRP) EXTERNAL_TOOLS["SPASS"] =str(spass_exe.resolve())print(f" OK SPASS installe: {spass_exe}") spass_archive.unlink(missing_ok=True) shutil.rmtree(spass_dir /"SPASS", ignore_errors=True)exceptExceptionas e:print(f" Erreur installation SPASS: {e}")elif system =="Darwin":print(" INFO SPASS non disponible en telechargement automatique pour macOS.")print(" Installez manuellement depuis: https://www.spass-prover.org/")
=== 2. Configuration de SPASS ===
INFO SPASS non configure.
Pour Windows, installez SPASS manuellement:
1. Telecharger depuis: https://www.spass-prover.org/download/binaries/
2. Choisir 'spass30windows.exe' et EXECUTER l'installeur
3. Copier SPASS.exe du repertoire d'installation vers:
ext_tools\spass
4. Re-executer cette cellule
Note: SPASS est OPTIONNEL. La logique modale fonctionne sans raisonnement.
1.5.3 EProver - Prouveur FOL de Haute Performance
E Prover est un prouveur automatique de theoremes pour la logique du premier ordre (FOL). C’est l’un des prouveurs les plus performants, regulierement gagnant des competitions CASC.
Utilisation dans Tweety : - logics.fol.reasoner.EFOLReasoner : Raisonnement FOL avance - Alternative a SimpleFolReasoner qui peut avoir des problemes de memoire
Note : EProver est fourni dans le depot (ext_tools/EProver/).
# === Configuration de EProver (prouveur FOL) ===print("=== 3. Configuration de EProver ===")eprover_search_paths = [ pathlib.Path("../ext_tools/EProver"), pathlib.Path("ext_tools/EProver"), pathlib.Path("../../ext_tools/EProver"),]eprover_exe_name ="eprover.exe"if system =="Windows"else"eprover"eprover_in_path = shutil.which("eprover") or shutil.which("eprover.exe")if eprover_in_path: EXTERNAL_TOOLS["EPROVER"] = eprover_in_pathprint(f" OK EProver trouve dans PATH: {eprover_in_path}")else:for search_path in eprover_search_paths: eprover_exe = search_path / eprover_exe_nameif eprover_exe.exists(): EXTERNAL_TOOLS["EPROVER"] =str(eprover_exe.resolve())print(f" OK EProver trouve: {eprover_exe.resolve()}")breakelse:print(" EProver non trouve dans les chemins standards.")print(" Telecharger depuis https://eprover.org/")
=== 3. Configuration de EProver ===
OK EProver trouve: <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\EProver\eprover.exe
1.5.4 Solveurs SAT - Satisfaction Booleenne
Les solveurs SAT sont au coeur de nombreuses fonctionnalites de Tweety : - Raisonnement en logique propositionnelle - Calcul des extensions d’argumentation (ADF) - Mesures d’incoherence
Hiérarchie des solveurs (du plus rapide au plus portable) :
Solveur
Type
Performance
Portabilite
CaDiCaL 1.9.5
Python (pySAT)
Champion SAT
Multi-plateforme
Lingeling
DLL native
Très rapide
Windows/Linux
MiniSat
DLL native
Rapide
Windows/Linux
PicoSAT
DLL native
Rapide
Windows/Linux
Sat4j
Pure Java
Modere
Multi-plateforme
Nouveau : Le wrapper sat_solver.py donne acces aux solveurs modernes via pySAT.
# === Configuration des solveurs SAT ===print("=== 4. Configuration des solveurs SAT ===")# 4.1 Bibliotheques SAT natives (pour ADF via JNI)print("\n--- 4.1 Bibliotheques SAT natives ---")if NATIVE_LIBS_DIR.exists():print(f" Repertoire libs/native: {NATIVE_LIBS_DIR.resolve()}") sat_libs_found = []for solver in ["lingeling", "minisat", "picosat"]: dll = NATIVE_LIBS_DIR /f"{solver}.dll" so = NATIVE_LIBS_DIR /f"{solver}.so"if dll.exists(): sat_libs_found.append(f"{solver}.dll")elif so.exists(): sat_libs_found.append(f"{solver}.so")if sat_libs_found:print(f" OK Bibliotheques trouvees: {', '.join(sat_libs_found)}")else:print(" Aucune bibliotheque native trouvee")else:print(" Repertoire libs/native non trouve")# 4.2 Sat4j (Pure Java - toujours disponible)print("\n--- 4.2 Sat4j (integre) ---")EXTERNAL_TOOLS["SAT_SOLVER"] ="Sat4j (integre)"print(" OK Sat4j disponible (org.tweetyproject.logics.pl.sat.Sat4jSolver)")# 4.3 Wrapper Python avec CaDiCaL et autres (nouveau!)print("\n--- 4.3 Wrapper Python SAT (CaDiCaL, Glucose, etc.) ---")sat_solver_paths = [ pathlib.Path("../ext_tools/sat_solver.py"), pathlib.Path("ext_tools/sat_solver.py"),]for sp in sat_solver_paths:if sp.exists(): EXTERNAL_TOOLS["SAT_SOLVER_PYTHON"] =str(sp.resolve())print(f" OK sat_solver.py trouve: {sp.resolve()}")try:from pysat.solvers import SolverNames solvers = ['cadical195', 'glucose42', 'maplechrono', 'lingeling'] available = [s for s in solvers ifhasattr(SolverNames, s)]print(f" OK Solveurs disponibles: {', '.join(available)}")exceptImportError:print(" WARN python-sat non disponible - redemarrez le noyau apres section 1.3")breakelse:print(" sat_solver.py non trouve")
=== 4. Configuration des solveurs SAT ===
--- 4.1 Bibliotheques SAT natives ---
Repertoire libs/native: <repo>MyIA.AI.Notebooks\SymbolicAI\libs\native
OK Bibliotheques trouvees: lingeling.dll, minisat.dll, picosat.dll
--- 4.2 Sat4j (integre) ---
OK Sat4j disponible (org.tweetyproject.logics.pl.sat.Sat4jSolver)
--- 4.3 Wrapper Python SAT (CaDiCaL, Glucose, etc.) ---
OK sat_solver.py trouve: <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\sat_solver.py
OK Solveurs disponibles: cadical195, glucose42, maplechrono, lingeling
1.5.5 MARCO et MaxSAT - Analyse d’Incoherence
Ces outils sont utilises pour l’analyse des bases de croyances incoherentes :
MARCO (MUS enumerator) : - Enumere les MUS (Minimal Unsatisfiable Subsets) et MCS (Maximal Consistent Subsets) - Utilise Z3 comme backend - Utilise par MarcoMusEnumerator dans Tweety
MaxSAT : - Resout le problème d’optimisation : maximiser le nombre de clauses satisfaites - Wrapper Python utilisant l’algorithme RC2 (gagnant MaxSAT Evaluation 2018) - Utilise par les mesures d’incoherence basees sur MinSum
# === Configuration de MARCO et MaxSAT ===print("=== 5. Configuration de MARCO (MUS enumerator) ===")marco_search_paths = [ pathlib.Path("../ext_tools/marco.py"), pathlib.Path("ext_tools/marco.py"),]for mp in marco_search_paths:if mp.exists(): EXTERNAL_TOOLS["MARCO"] =str(mp.resolve())print(f" OK MARCO trouve: {mp.resolve()}")try:import z3print(f" OK Z3 disponible (version {z3.get_version_string()})")exceptImportError:print(" WARN z3 non disponible - redemarrez le noyau apres section 1.3")breakelse:print(" MARCO non trouve")print("\n=== 6. Configuration de MaxSAT ===")maxsat_search_paths = [ pathlib.Path("../ext_tools/maxsat_solver.py"), pathlib.Path("ext_tools/maxsat_solver.py"),]for mp in maxsat_search_paths:if mp.exists(): EXTERNAL_TOOLS["OPEN_WBO"] =str(mp.resolve())print(f" OK MaxSAT solver trouve: {mp.resolve()}")try:import pysatprint(f" OK python-sat disponible (RC2 algorithm)")exceptImportError:print(" WARN python-sat non disponible - redemarrez le noyau apres section 1.3")breakelse:print(" MaxSAT solver non trouve")# === Resume final ===print("\n"+"="*50)print("RESUME DES OUTILS EXTERNES")print("="*50)for tool, path in EXTERNAL_TOOLS.items(): status ="OK"if (path and (path.startswith("Sat4j") or get_tool_path(tool))) else"Non configure" display_path = path[:50] +"..."if path andlen(path) >50else (path or"-")print(f" {tool:<18}: [{status:^12}] {display_path}")print("="*50)
=== 5. Configuration de MARCO (MUS enumerator) ===
OK MARCO trouve: <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\marco.py
OK Z3 disponible (version 4.16.0)
=== 6. Configuration de MaxSAT ===
OK MaxSAT solver trouve: <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\maxsat_solver.py
OK python-sat disponible (RC2 algorithm)
==================================================
RESUME DES OUTILS EXTERNES
==================================================
SAT_SOLVER : [ OK ] Sat4j (integre)
SAT_SOLVER_PYTHON : [ OK ] <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\...
EPROVER : [ OK ] <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\...
MARCO : [ OK ] <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\...
OPEN_WBO : [ OK ] <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\...
CLINGO : [ OK ] <repo>MyIA.AI.Notebooks\SymbolicAI\Tweety\ext...
SPASS : [Non configure] -
==================================================
1.6 Démarrage de la JVM via JPype
JPype permet à Python d’interagir directement avec le code Java. Nous devons démarrer une Machine Virtuelle Java (JVM) et lui indiquer où trouver les fichiers JAR de Tweety que nous venons de télécharger.
Le code tente de trouver votre JAVA_HOME. Modifiez java_home_path si nécessaire dans la cellule suivante.
Il construit le classpath Java en listant tous les .jar dans le dossier libs/.
jpype.startJVM() lance la JVM. Si elle est déjà lancée (ex: après redémarrage du noyau), l’appel est ignoré.
Crucial: jpype.imports.registerDomain(...) doit être appelé après le démarrage de la JVM pour permettre les imports courts (ex: from org.tweetyproject...).
Récapitulatif de la configuration des outils externes
État de l’environnement : Si vous avez exécuté toutes les cellules de configuration des outils, vous disposez maintenant de :
Outil
Statut
Impact si absent
Clingo
Configuré automatiquement
ASP (Answer Set Programming) indisponible
SPASS
Détecté ou guide d’installation
Logique modale : SimpleMlReasoner peut bloquer
EProver
Détecté dans ext_tools/
Raisonnement FOL limité à SimpleFolReasoner
SAT solvers
Multiple (Sat4j, CaDiCaL, natifs)
Performances SAT réduites
MARCO
Script Python avec Z3
Énumération MUS indisponible
MaxSAT
RC2 via python-sat
Optimisation MaxSAT indisponible
Points clés :
Sat4j (pure Java) est toujours disponible - c’est le solveur SAT de secours
CaDiCaL (via pySAT) offre les meilleures performances pour les problèmes SAT modernes
Bibliothèques natives (Lingeling, MiniSat, PicoSAT) sont utilisées pour ADF via JNI
Note : La plupart des exemples de la série Tweety fonctionnent avec la configuration minimale (Sat4j). Les outils externes sont requis uniquement pour les sections avancées spécifiques.
Prochaine étape : Démarrage de la Machine Virtuelle Java (JVM) pour accéder aux classes TweetyProject.
1.6.1 Fonctions Utilitaires JDK
Avant de demarrer la JVM, nous definissons des fonctions pour localiser ou telecharger automatiquement un JDK compatible.
Stratégie de detection JDK (par ordre de priorite) : 1. JDK portable existant dans jdk-17-portable/ 2. Telechargement automatique de Zulu JDK 17 (Azul) 3. Variable d’environnement JAVA_HOME 4. Detection automatique des JDKs système
# --- 1.6.1 Fonctions Utilitaires JDK ---import jpypeimport jpype.importsimport osimport pathlibimport platformimport urllib.requestimport zipfileimport shutilfrom jpype.types import*import stat# URLs de telechargement Zulu JDK 17 (Azul)JDK_DOWNLOAD_URLS = {"Windows": "https://cdn.azul.com/zulu/bin/zulu17.50.19-ca-jdk17.0.11-win_x64.zip","Linux": "https://cdn.azul.com/zulu/bin/zulu17.50.19-ca-jdk17.0.11-linux_x64.tar.gz","Darwin": "https://cdn.azul.com/zulu/bin/zulu17.50.19-ca-jdk17.0.11-macosx_x64.zip"}def find_portable_jdk():"""Localise le JDK portable dans l'arborescence du projet."""print("Recherche JDK portable dans l'arborescence projet...") search_paths = [ pathlib.Path("jdk-17-portable"), pathlib.Path("../jdk-17-portable"), pathlib.Path("../Argument_Analysis/jdk-17-portable"), pathlib.Path("../../jdk-17-portable"), ] exe_suffix =".exe"if platform.system() =="Windows"else""for base_path in search_paths:if base_path.exists():for pattern in ["*jdk*", "zulu*"]:for jdk_dir in base_path.glob(pattern):if jdk_dir.is_dir(): java_exe = jdk_dir /"bin"/f"java{exe_suffix}"if java_exe.exists():print(f" OK JDK portable trouve: {jdk_dir.absolute()}")returnstr(jdk_dir.absolute())print(" JDK portable non trouve")returnNonedef download_portable_jdk():"""Telecharge et extrait le JDK portable Zulu 17.""" system = platform.system()if system notin JDK_DOWNLOAD_URLS:print(f"Systeme {system} non supporte pour telechargement auto")returnNone url = JDK_DOWNLOAD_URLS[system] jdk_dir = pathlib.Path("jdk-17-portable") jdk_dir.mkdir(exist_ok=True) archive_name = url.split("/")[-1] archive_path = jdk_dir / archive_nameprint(f"Telechargement JDK depuis {url}...")try: urllib.request.urlretrieve(url, archive_path)print(f"Extraction de {archive_name}...")if archive_name.endswith(".zip"):with zipfile.ZipFile(archive_path, 'r') as zf: zf.extractall(jdk_dir)elif archive_name.endswith(".tar.gz"):import tarfilewith tarfile.open(archive_path, 'r:gz') as tf: tf.extractall(jdk_dir) archive_path.unlink()return find_portable_jdk()exceptExceptionas e:print(f"Erreur telechargement JDK: {e}")returnNoneprint("Fonctions JDK definies: find_portable_jdk(), download_portable_jdk()")
Cette cellule detecte le JDK disponible et le telecharge si necessaire.
Important : JPype necessite un JDK 11+ (JDK 17 recommande pour Tweety 1.30).
# --- 1.6.2 Detection du JDK ---def find_java_home():"""Trouve JAVA_HOME selon la strategie de priorite."""# 1. JDK portable existant portable_jdk = find_portable_jdk()if portable_jdk: os.environ['JAVA_HOME'] = portable_jdkreturn portable_jdk# 2. Telechargement automatiqueprint("JDK portable non trouve - telechargement automatique...") downloaded_jdk = download_portable_jdk()if downloaded_jdk: os.environ['JAVA_HOME'] = downloaded_jdkreturn downloaded_jdk# 3. Variable JAVA_HOME java_home_env = os.getenv("JAVA_HOME") exe_suffix =".exe"if platform.system() =="Windows"else""if java_home_env and pathlib.Path(java_home_env).is_dir():if (pathlib.Path(java_home_env) /"bin"/f"java{exe_suffix}").exists():print(f" Utilisation JAVA_HOME: {java_home_env}")return java_home_env# 4. Detection systemeprint("Detection automatique des JDKs systeme...") possible_locations = []if platform.system() =="Windows": java_dir = pathlib.Path("C:/Program Files/Java/")if java_dir.is_dir(): possible_locations =sorted(java_dir.glob("jdk-*/"), reverse=True)elif platform.system() =="Linux":for p_str in ["/usr/lib/jvm"]: p_obj = pathlib.Path(p_str)if p_obj.is_dir(): possible_locations.extend(sorted(p_obj.glob("java-*"), reverse=True))for p in possible_locations: java_bin = p /"bin"/f"java{exe_suffix}"if java_bin.exists():print(f" JDK systeme detecte: {p}") os.environ['JAVA_HOME'] =str(p)returnstr(p)print("ERREUR: Aucun JDK trouve ou telechargeable")returnNone# Executer la detectionjava_home_path = find_java_home()if java_home_path:print(f"\nJAVA_HOME configure: {java_home_path}")
Recherche JDK portable dans l'arborescence projet...
OK JDK portable trouve: <repo>MyIA.AI.Notebooks\SymbolicAI\Tweety\jdk-17-portable\zulu17.50.19-ca-jdk17.0.11-win_x64
JAVA_HOME configure: <repo>MyIA.AI.Notebooks\SymbolicAI\Tweety\jdk-17-portable\zulu17.50.19-ca-jdk17.0.11-win_x64
1.6.3 Construction du Classpath
Le classpath indique a la JVM ou trouver les classes Java. Nous assemblons tous les JARs Tweety du dossier libs/.
# --- 1.6.3 Construction du Classpath ---classpath_separator = os.pathsepif'LIB_DIR'notinglobals(): LIB_DIR = pathlib.Path("libs")jar_list = [str(p.resolve()) for p in LIB_DIR.glob("*.jar")]num_jars_found =len(jar_list)ifnot jar_list:print("ERREUR: Aucun JAR trouve dans libs/") classpath =""else: classpath = classpath_separator.join(jar_list)print(f"Classpath assemble: {num_jars_found} JARs")# Verification presence JAR beliefdynamics beliefdynamics_found =any("beliefdynamics"in j for j in jar_list)if beliefdynamics_found:print(" OK JAR beliefdynamics present")else:print(" ATTENTION: JAR beliefdynamics non trouve")
Classpath assemble: 42 JARs
OK JAR beliefdynamics present
1.6.4 Demarrage de la JVM
Important : Si des JARs ont ete telecharges dans les cellules précédentes, redemarrez le noyau avant d’executer cette cellule.
La JVM est demarree une seule fois par session Python. Une fois demarree, toutes les classes Java sont accessibles via les imports Python.
# --- 1.6.4 Demarrage de la JVM ---ifnot jpype.isJVMStarted():ifnot java_home_path:print("ERREUR: Impossible de demarrer la JVM sans JAVA_HOME")elif num_jars_found ==0:print("ERREUR: Classpath vide - verifiez le dossier libs/")else:print("Demarrage de la JVM...") jvm_args = ["-ea", f"-Djava.class.path={classpath}"]# Ajouter bibliotheques natives si presentesif'NATIVE_LIBS_DIR'inglobals() and NATIVE_LIBS_DIR.exists(): jvm_args.append(f"-Djava.library.path={NATIVE_LIBS_DIR.resolve()}")print(f" Avec bibliotheques natives: {NATIVE_LIBS_DIR}")try: jpype.startJVM(*jvm_args, convertStrings=False) jpype.imports.registerDomain("org") jpype.imports.registerDomain("java") jpype.imports.registerDomain("net")print("OK JVM demarree et domaines enregistres")exceptExceptionas e:print(f"ERREUR demarrage JVM: {e}")else:print("JVM deja en cours d'execution")
Demarrage de la JVM...
Avec bibliotheques natives: ..\libs\native
OK JVM demarree et domaines enregistres
1.6.5 Verification des Imports Java
Verification que les classes Tweety essentielles sont accessibles.
Note sur InformationObject : Dans Tweety 1.30, cette classe se trouve dans org.tweetyproject.beliefdynamics.mas.InformationObject (package mas). CrMas et la Revision de Croyances multi-agents fonctionnent normalement.
# --- 1.6.5 Verification des Imports ---print("Test des imports Java essentiels...")CrMas_Imports_OK =False# Variable utilisee par les autres notebooksif jpype.isJVMStarted(): imports_ok =True missing = []# Test InformationObject (dans le package 'mas' depuis Tweety 1.28+)try:from org.tweetyproject.beliefdynamics.mas import InformationObject, CrMasBeliefSet, CrMasRevisionWrapperprint(" OK InformationObject (org.tweetyproject.beliefdynamics.mas)")print(" OK CrMasBeliefSet")print(" OK CrMasRevisionWrapper") CrMas_Imports_OK =TrueexceptImportErroras e:print(f" INFO CrMas imports incomplets: {e}")print(" Impact: Seule la section CrMas sera desactivee.")# Tests critiques (doivent tous reussir)try:from org.tweetyproject.commons import Formulaprint(" OK commons.Formula")exceptImportError: missing.append("commons.Formula") imports_ok =Falsetry:from org.tweetyproject.logics.pl.syntax import Proposition, PlFormulaprint(" OK logics.pl.syntax (Proposition, PlFormula)")exceptImportError: missing.append("logics.pl.syntax") imports_ok =Falsetry:from org.tweetyproject.arg.dung.syntax import Argument, DungTheoryprint(" OK arg.dung.syntax (Argument, DungTheory)")exceptImportError: missing.append("arg.dung.syntax") imports_ok =Falsetry:from java.util import ArrayList, HashSetprint(" OK java.util (ArrayList, HashSet)")exceptImportError: missing.append("java.util") imports_ok =False# Resumeprint("")if imports_ok:print("Tous les imports critiques sont disponibles.")print("Tweety est pret a etre utilise!")else:print(f"ERREUR: Imports manquants: {', '.join(missing)}")print("Verifiez les JARs dans libs/")# Afficher le statut CrMas tweety_ver =globals().get('TWEETY_VERSION', 'inconnue')print(f"\nVersion Tweety: {tweety_ver}")print(f"CrMas_Imports_OK = {CrMas_Imports_OK}")ifnot CrMas_Imports_OK:print("(Les sections CrMas seront sautees automatiquement)")else:print("JVM non demarree - impossible de tester les imports")
Test des imports Java essentiels...
OK InformationObject (org.tweetyproject.beliefdynamics.mas)
OK CrMasBeliefSet
OK CrMasRevisionWrapper
OK commons.Formula
OK logics.pl.syntax (Proposition, PlFormula)
OK arg.dung.syntax (Argument, DungTheory)
OK java.util (ArrayList, HashSet)
Tous les imports critiques sont disponibles.
Tweety est pret a etre utilise!
Version Tweety: inconnue
CrMas_Imports_OK = True
1.7 Concepts Clés de Tweety et JPype
Avant de plonger dans les exemples, comprenons quelques concepts fondamentaux de Tweety et comment nous interagissons avec eux via JPype :
Concepts Tweety :
Signature (org.tweetyproject.logics.[logic].syntax.[Logic]Signature) : Définit le vocabulaire d’une logique.
Formula (org.tweetyproject.logics.[logic].syntax.[Logic]Formula) : Représente une formule bien formée.
BeliefBase (org.tweetyproject.logics.[logic].syntax.[Logic]BeliefSet) : Un ensemble de formules (base de connaissances).
Interpretation (org.tweetyproject.logics.[logic].semantics.Interpretation) : Assigne une signification sémantique (ex: PossibleWorld).
Parser (org.tweetyproject.logics.[logic].parser.[Logic]Parser) : Analyse chaînes/fichiers vers Formula/BeliefSet.
Reasoner (org.tweetyproject.logics.[logic].reasoner.[Logic]Reasoner) : Implémente le raisonnement (query, getModels). Des raisonneurs par défaut peuvent être définis.
Argumentation Frameworks (org.tweetyproject.arg.*): Classes pour les cadres (DungTheory, AspicArgumentationTheory, etc.) et composants (Argument, Attack, Support).
Interaction Python-Java avec JPype :
Imports: Grâce à jpype.imports.registerDomain("org", alias="org") (exécuté dans la cellule de démarrage JVM), on peut importer les classes Java comme des modules Python :
from org.tweetyproject.logics.pl.syntax import Propositionfrom org.tweetyproject.arg.dung.syntax import Argument, Attackfrom java.util import ArrayList # Également possible via registerDomain("java", alias="java")
Instanciation: p = Proposition("a").
Appel de Méthodes: kb.add(p).
Types Primitifs: Conversion auto (int, float, bool, str).
Collections Java: Utiliser les types Java explicites (ArrayList, HashSet depuis java.util).
Surcharge (Overloading): Si ambiguïté, caster avec JObject(variable, ClasseJava) ou JInt(), JString(), etc. (depuis jpype.types).
Exceptions Java: Attraper avec except jpype.JException as e_java:. Accéder au message avec e_java.message() et à la trace avec e_java.stacktrace().
Resume
Ce notebook a configure l’environnement complet TweetyProject pour la serie de notebooks sur l’IA symbolique.
Tous les outils necessaires pour la serie de notebooks sont maintenant operationnels :
Outil
Utilisation
Notebooks concernes
SPASS
Raisonnement modal (Box/Diamond)
Tweety-3 (Logiques Avancees)
EProver
Raisonnement FOL avance
Tweety-2 (Logiques de Base)
Clingo
Answer Set Programming
Tweety-6 (Argumentation Structuree)
CaDiCaL
SAT solving moderne
Tweety-2, Tweety-4
MARCO
Enumeration MUS/MCS
Tweety-4 (Revision de Croyances)
MaxSAT (RC2)
Optimisation satisfiabilite
Tweety-4 (Incoherence)
Points cles a retenir
Architecture JPype : Pont Python-Java pour interfacer avec les bibliotheques Java de Tweety
Classpath JVM : Tous les JARs du dossier libs/ sont charges au demarrage
Imports Java : Utiliser from org.tweetyproject... après registerDomain()
Outils externes : Optionnels mais recommandes pour les fonctionnalites avancees
Portabilite : JDK portable Zulu 17 inclus (pas de configuration système requise)
Dependances externes : SAT4J et args4j inclus dans libs/ (necessaires pour v1.30)
Verification de l’installation
Si tous les messages “OK” sont presents dans les cellules précédentes, l’environnement est pret.
Tests de validation : - JVM demarree : jpype.isJVMStarted() retourne True - Imports critiques : commons.Formula, logics.pl.syntax, arg.dung.syntax - Outils externes : configures dans le resume final (section 1.5)
Note : Si certains outils externes ne sont pas disponibles, les notebooks correspondants afficheront des avertissements mais resteront executables avec des alternatives internes.
Prochaines étapes
L’environnement etant configure, vous pouvez maintenant explorer :
Tweety-2-Basic-Logics : Logique propositionnelle et FOL (premiers pas)
Tweety-5-Abstract-Argumentation : Frameworks de Dung et sémantiques (equiv. + explications v1.30)
Tweety-6-Structured-Argumentation : ASPIC+, DeLP, ABA, ASP
Chaque notebook utilise les composants installes ici et ne necessite pas de configuration supplementaire.
Exercice : Validez votre installation Tweety
Avant de passer aux notebooks suivants, verifiez votre maitrise de l’environnement TweetyProject configure dans ce notebook.
Exercice - Diagnostic de l’environnement
Ecrivez une cellule de diagnostic qui :
Importe jpype et affiche sa version
Verifie que la JVM est demarree (jpype.isJVMStarted())
Importe une classe Tweety simple (par exemple PlBeliefSet du package org.tweetyproject.logics.pl.syntax) et l’instancie
Completez le squelette ci-dessous.
Indice : reprenez les imports de la section 1.6.5 (Verification des Imports). Si la JVM n’est pas demarree, re-executez d’abord la cellule 1.6.4 (Demarrage de la JVM).
# Exercice de validation - Diagnostic de l'environnement Tweety# Completez les TODO ci-dessous pour verifier votre installation.# TODO etudiant : importer jpype et afficher sa version# TODO etudiant : verifier que la JVM est demarree (jpype.isJVMStarted())# TODO etudiant : importer une classe Tweety (ex: PlBeliefSet) et l'instancierprint("Exercice a completer")
Exercice a completer
Notebooks de la série Tweety
Après avoir exécuté ce notebook de configuration, vous pouvez explorer: