Logiques de Base - Propositionnelle et Premier Ordre

Navigation: ← Tweety-1-Setup | Index | Tweety-3-Advanced-Logics →

Objectifs pédagogiques

  1. Maîtriser la syntaxe et le parsing des formules propositionnelles (PL)
  2. Comprendre les mondes possibles et la satisfiabilité
  3. Utiliser le solveur SAT4J intégré à Tweety
  4. Découvrir la logique du premier ordre (FOL) avec prédicats et quantificateurs

Prérequis

Exécutez d’abord Tweety-01-Setup-Python.ipynb pour configurer l’environnement JVM.

Durée estimée : 45 minutes

Limitations connues (Tweety 1.28): - FOL avec égalité peut causer des problèmes de heap space avec SimpleFolReasoner - Préférer EProver pour les requêtes FOL complexes

# --- Initialisation JVM Tweety + Outils Externes ---
print("--- Verification JVM Tweety + Outils ---")
jvm_ready = False

import jpype
import jpype.imports
import os
import pathlib
import shutil
import platform

# === Configuration COMPLETE des outils externes ===
EXTERNAL_TOOLS = {
    "CLINGO": "",
    "SPASS": "",
    "EPROVER": "",           # Nouveau: prouveur FOL
    "SAT_SOLVER_PYTHON": "", # Nouveau: wrapper pySAT
    "MARCO": "",             # Nouveau: MUS enumerator
}

def get_tool_path(tool_name):
    """Retourne le chemin valide d'un outil ou None."""
    path_str = EXTERNAL_TOOLS.get(tool_name, "")
    if not path_str: 
        return None
    if shutil.which(path_str):
        return path_str
    path_obj = pathlib.Path(path_str)
    if path_obj.is_file():
        return str(path_obj.resolve())
    if path_obj.is_dir():
        return str(path_obj.resolve())
    return None

# --- Auto-detection des outils ---
system = platform.system()
exe_suffix = ".exe" if system == "Windows" else ""

# 1. Clingo (ASP solver)
for cp in [shutil.which("clingo"), pathlib.Path(f"ext_tools/clingo/clingo{exe_suffix}"),
           pathlib.Path(f"../ext_tools/clingo/clingo{exe_suffix}")]:
    if cp and (isinstance(cp, str) or cp.exists()):
        EXTERNAL_TOOLS["CLINGO"] = str(pathlib.Path(cp).parent.resolve()) if isinstance(cp, pathlib.Path) else str(pathlib.Path(cp).parent)
        break

# 2. SPASS (Modal logic prover)
for sp in [shutil.which("SPASS"), pathlib.Path(f"ext_tools/spass/SPASS{exe_suffix}"),
           pathlib.Path(f"../ext_tools/spass/SPASS{exe_suffix}")]:
    if sp and (isinstance(sp, str) or sp.exists()):
        EXTERNAL_TOOLS["SPASS"] = str(pathlib.Path(sp).resolve()) if isinstance(sp, pathlib.Path) else sp
        break

# 3. EProver (FOL theorem prover) - NOUVEAU
for ep in [shutil.which("eprover"), pathlib.Path(f"../ext_tools/EProver/eprover{exe_suffix}"),
           pathlib.Path(f"../../ext_tools/EProver/eprover{exe_suffix}")]:
    if ep:
        ep_path = pathlib.Path(ep) if isinstance(ep, str) else ep
        if ep_path.exists():
            EXTERNAL_TOOLS["EPROVER"] = str(ep_path.resolve())
            break

# 4. SAT Solver Python (CaDiCaL, Glucose via pySAT) - NOUVEAU
for sat in [pathlib.Path("../ext_tools/sat_solver.py"), pathlib.Path("../../ext_tools/sat_solver.py")]:
    if sat.exists():
        EXTERNAL_TOOLS["SAT_SOLVER_PYTHON"] = str(sat.resolve())
        break

# 5. MARCO (MUS enumerator) - NOUVEAU
for mp in [pathlib.Path("../ext_tools/marco.py"), pathlib.Path("../../ext_tools/marco.py")]:
    if mp.exists():
        EXTERNAL_TOOLS["MARCO"] = str(mp.resolve())
        break

# === Initialisation JVM ===
if jpype.isJVMStarted():
    print("JVM deja en cours d'execution.")
    jvm_ready = True
else:
    # Chercher JDK portable
    jdk_portable = None
    for jdk_path in [pathlib.Path("jdk-17-portable"), pathlib.Path("../Argument_Analysis/jdk-17-portable")]:
        if jdk_path.exists():
            zulu_dirs = list(jdk_path.glob("zulu*"))
            if zulu_dirs:
                jdk_portable = zulu_dirs[0]
                os.environ["JAVA_HOME"] = str(jdk_portable.resolve())
                print(f"JDK portable: {jdk_portable.name}")
                break
    
    if not os.environ.get("JAVA_HOME"):
        print("ERREUR: JAVA_HOME non defini et JDK portable non trouve.")
    else:
        LIB_DIR = pathlib.Path("libs")
        if not LIB_DIR.exists():
            LIB_DIR = pathlib.Path("../Argument_Analysis/libs")
        
        if LIB_DIR.exists():
            jar_files = list(LIB_DIR.glob("*.jar"))
            if jar_files:
                classpath = os.pathsep.join(str(j.resolve()) for j in jar_files)
                try:
                    jpype.startJVM(classpath=[classpath])
                    print(f"JVM demarree avec {len(jar_files)} JARs.")
                    jvm_ready = True
                except Exception as e:
                    print(f"Erreur demarrage JVM: {e}")

# === Resume des outils ===
if jvm_ready:
    print("\n--- Outils disponibles ---")
    tools_status = []
    for tool, path in EXTERNAL_TOOLS.items():
        if path:
            short_path = path.split(os.sep)[-1] if len(path) > 30 else path
            tools_status.append(f"{tool}: OK")
            print(f"  {tool}: {short_path}")
        else:
            tools_status.append(f"{tool}: -")
    print(f"\nJVM prete. Outils: {sum(1 for t,p in EXTERNAL_TOOLS.items() if p)}/{len(EXTERNAL_TOOLS)}")
--- Verification JVM Tweety + Outils ---
JDK portable: zulu17.50.19-ca-jdk17.0.11-win_x64
JVM demarree avec 10 JARs.

--- Outils disponibles ---
  EPROVER: eprover.exe
  SAT_SOLVER_PYTHON: sat_solver.py
  MARCO: marco.py

JVM prete. Outils: 3/5

Interpretation de l’initialisation JVM

Succes de l’initialisation : - JVM demarree avec 10 JARs charges - JDK portable Zulu 17 detecte et utilise - 3/5 outils externes detectes (EPROVER, SAT_SOLVER_PYTHON, MARCO)

Outils externes (cartographie des roles ; 3/5 detectes sur ce run, cf cellule precedente) :

Outil Rôle Utilisation
CLINGO Solveur ASP (Answer Set Programming) Logique ASP (notebook 6)
SPASS Prouveur de theoremes modal Logique modale (notebook 3)
EPROVER Prouveur FOL (First-Order Logic) Logique du premier ordre (section 2.2)
SAT_SOLVER_PYTHON Wrapper pySAT (CaDiCaL, Glucose) Solveurs SAT modernes (section 2.1.3)
MARCO Enumerateur MUS (Minimal Unsatisfiable Subsets) Analyse d’incohérences (notebook 4)

Importance de la detection automatique : - Les outils sont cherches dans ext_tools/ et dans le PATH système - Si un outil manque, Tweety utilise un fallback (ex: SAT4J au lieu de CaDiCaL) - Cette approche permet de fonctionner partout tout en beneficiant d’outils externes quand disponibles

Note : Pour les notebooks suivants, EProver et pySAT seront particulierement utiles.

Note de parite cross-langage (EPIC #4956) : Le jumeau C# de ce notebook (voir Tweety-02-Basic-Logics-CSharp.ipynb) utilise une strategie differente : IKVM transpile statiquement le bytecode Java de Tweety en DLL .NET native (7 Mo), tandis que ce notebook Python utilise jpype pour demarrer une JVM in-process et appeler directement les classes Java. Les deux strategies donnent acces au meme API Tweety (Proposition, PlBeliefSet, PlParser, FolReasoner…). Audit c.739 (2026-07-22) : 0 doc-honesty finding corrigible des deux cotes.

Partie 2 : Logiques Fondamentales dans Tweety

Explorons comment représenter et raisonner avec certaines logiques de base en utilisant Tweety via JPype.

2.1 Logique Propositionnelle (PL)

La logique propositionnelle est la fondation de nombreux systèmes de raisonnement. Elle permet de représenter des faits et des relations logiques entre eux.

Pourquoi la logique propositionnelle ? - Base de tous les systèmes de raisonnement automatique - Fondement des solveurs SAT (utilisés en vérification, planification, argumentation) - Suffisante pour modéliser de nombreux problèmes combinatoires

Concepts Clés :

Concept Classe Tweety Syntaxe Exemple
Proposition Proposition lettre a, pluie
Négation Negation ! !a = “non a”
Conjonction Conjunction && a && b = “a et b”
Disjonction Disjunction \|\| a \|\| b = “a ou b”
Implication Implication => a => b = “si a alors b”
Équivalence Equivalence <=> a <=> b = “a ssi b”
Xor ExclusiveDisjunction ^^ a ^^ b = “a ou b mais pas les deux”

Tables de vérité (rappel):

a b a && b a || b a => b !a
0 0 0 0 1 1
0 1 0 1 1 1
1 0 0 1 0 0
1 1 1 1 1 0

Classes principales: * PlFormula: Interface/classe de base pour toutes les formules PL * PlBeliefSet: Un ensemble de formules (base de connaissances) * PossibleWorld: Une assignation de vérité aux propositions (interprétation) * PlParser: Analyse syntaxique de chaînes vers formules * Raisonnement: SimplePlReasoner (énumération), SatSolver (SAT4J, etc.)

2.1.1 Syntaxe, Parsing, Mondes Possibles

Voyons comment créer, parser et évaluer des formules PL.

# --- 2.1.1a Imports et verification JVM ---
print("--- 2.1.1 Logique Propositionnelle : Setup ---")

# Verification de la JVM
jvm_ready = False
try:
    import jpype
    if jpype.isJVMStarted():
        from org.tweetyproject.logics.pl.syntax import Proposition
        jvm_ready = True
        print("JVM prete.")
except Exception as e:
    print(f"Erreur: {e}")

if not jvm_ready:
    print("ERREUR: JVM non demarree. Executez d'abord la cellule d'initialisation.")
else:
    # Imports Tweety pour la logique propositionnelle
    from jpype.types import JObject
    from java.util import ArrayList, Collection

    from org.tweetyproject.logics.pl.syntax import (
        PlBeliefSet, Proposition, Negation, Conjunction,
        Implication, Disjunction, Equivalence, PlFormula,
        Contradiction, Tautology, PlSignature
    )
    from org.tweetyproject.logics.pl.parser import PlParser
    from org.tweetyproject.logics.pl.semantics import PossibleWorld
    from org.tweetyproject.logics.pl.sat import DimacsSatSolver

    # Classes Java pour les casts
    Collection_class = jpype.JClass("java.util.Collection")
    PlFormula_class = jpype.JClass("org.tweetyproject.logics.pl.syntax.PlFormula")

    # Parser global
    pl_parser = PlParser()

    print("Imports PL reussis. Classes disponibles:")
    print("  - Proposition, Negation, Conjunction, Disjunction, Implication")
    print("  - PlBeliefSet, PlParser, PossibleWorld")
--- 2.1.1 Logique Propositionnelle : Setup ---
JVM prete.
Imports PL reussis. Classes disponibles:
  - Proposition, Negation, Conjunction, Disjunction, Implication
  - PlBeliefSet, PlParser, PossibleWorld

Interpretation de l’initialisation PL

Succes : La JVM est prete et les classes PL ont ete chargees.

Classes disponibles : - Proposition, Negation, Conjunction, Disjunction, Implication : Constructeurs de formules - PlBeliefSet : Base de connaissances (ensemble de formules) - PlParser : Parsing de formules depuis des chaînes - PossibleWorld : Interpretations (assignations de verite)

Architecture Tweety pour PL :

PlSignature (vocabulaire : ensemble de propositions)
     |
PlFormula (syntaxe : arbres de formules)
     |
PlBeliefSet (base de connaissances)
     |
PlReasoner (sémantique : inference logique)

Note : Le package org.tweetyproject.logics.pl.* contient toute la logique propositionnelle. Pour d’autres logiques (FOL, Description Logic), les packages changent mais la structure reste similaire.

Construction manuelle de formules

On peut construire des formules de deux facons: 1. Par API Java: en creant des objets Proposition, Negation, etc. 2. Par parsing: en utilisant PlParser pour parser une chaîne

Exemple de construction manuelle:

# --- 2.1.1b Construction manuelle de formules ---
if jvm_ready:
    # Creer des propositions atomiques
    a = Proposition("a")
    b = Proposition("b")
    c = Proposition("c")
    d = Proposition("d")

    # Construire des formules complexes
    f1 = a                           # a
    f2 = Negation(b)                 # !b
    f3 = Conjunction(a, Negation(c)) # a && !c
    f4 = Implication(a, b)           # a => b

    # Disjunction necessite une ArrayList
    list_cd = ArrayList()
    list_cd.add(c)
    list_cd.add(d)
    f5 = Disjunction(list_cd)        # c || d

    # Creer une base de connaissances (Knowledge Base)
    kb_manual = PlBeliefSet()
    kb_manual.add(f1)
    kb_manual.add(f2)
    kb_manual.add(f3)
    kb_manual.add(f4)
    kb_manual.add(f5)

    print("KB construite manuellement:")
    print(f"  {kb_manual}")
    print(f"\nFormules individuelles:")
    print(f"  f1 = {f1} (proposition)")
    print(f"  f2 = {f2} (negation)")
    print(f"  f3 = {f3} (conjonction)")
    print(f"  f4 = {f4} (implication)")
    print(f"  f5 = {f5} (disjonction)")
else:
    print("Cellule sautee : JVM Tweety non disponible")
KB construite manuellement:
  { a&&!c, (a=>b), c||d, a, !b }

Formules individuelles:
  f1 = a (proposition)
  f2 = !b (negation)
  f3 = a&&!c (conjonction)
  f4 = (a=>b) (implication)
  f5 = c||d (disjonction)

Interpretation de la KB construite manuellement

Sortie obtenue :

KB = { a&&!c, (a=>b), c||d, a, !b }

Analyse de consistance :

Formules de la KB : 1. a → a est vrai 2. !b → b est faux 3. a && !c → a vrai ET c faux 4. a => b → si a alors b 5. c || d → c ou d (au moins un)

Verification de coherence : - De (1) et (4) : a est vrai, donc a => b implique b vrai - Mais (2) dit !b (b est faux) - CONTRADICTION : Cette KB est insatisfiable !

Point pedagogique : - La construction manuelle permet des formules inconsistantes - C’est voulu pour illustrer la notion de consistance vs inconsistance - Un solveur SAT retournerait UNSAT pour cette KB

Astuce : Toujours verifier la consistance d’une KB avec solver.isSatisfiable(kb) avant de faire des requêtes.

Parsing de formules

Le PlParser permet de parser des formules depuis des chaînes de caractères. La syntaxe utilise les opérateurs: - ! pour la negation - && pour la conjonction - || pour la disjonction - => pour l’implication - <=> pour l’equivalence - ^^ pour le XOR (ou exclusif)

# --- 2.1.1c Parsing de formules ---
if jvm_ready:
    # Parser une base de connaissances depuis une chaine
    # IMPORTANT: Le parser Tweety est sensible aux espaces de debut de ligne.
    # Utiliser le format compact avec \n comme separateur de formules.
    kb_str = "a || b || c\n!a || b\n!b || c"
    
    kb_parsed = pl_parser.parseBeliefBase(kb_str)
    print(f"KB parsee depuis chaine:")
    print(f"  {kb_parsed}")

    # Parser une formule XOR
    formula_xor = pl_parser.parseFormula("a ^^ b ^^ c")
    print(f"\nFormule XOR: {formula_xor}")
    print(f"  Forme DNF: {formula_xor.toDnf()}")

    # La DNF (Disjunctive Normal Form) montre les 4 interpretations
    # qui rendent a XOR b XOR c vrai:
    # - a=T, b=F, c=F
    # - a=F, b=T, c=F
    # - a=F, b=F, c=T
    # - a=T, b=T, c=T
else:
    print("JVM non demarree - cellule sautee")
KB parsee depuis chaine:
  { !a||b, !b||c, a||b||c }

Formule XOR: a^^b^^c
  Forme DNF: (!b&&a&&!c)||(!a&&b&&!c)||(!a&&!b&&c)||(a&&b&&c)

Interpretation du parsing et de la DNF

KB parsee : { !a||b, !b||c, a||b||c }

Cette KB encode une chaîne d’implications : - !a||b = a => b (si a alors b) - !b||c = b => c (si b alors c) - Donc : a => b => c

Formule XOR parsee : a ^^ b ^^ c

Forme DNF (Disjunctive Normal Form) :

(!b&&a&&!c) || (!a&&b&&!c) || (!a&&!b&&c) || (a&&b&&c)

Interpretation de la DNF : La DNF liste explicitement tous les cas ou la formule est vraie : 1. a=T, b=F, c=F → 1 variable vraie 2. a=F, b=T, c=F → 1 variable vraie 3. a=F, b=F, c=T → 1 variable vraie 4. a=T, b=T, c=T → 3 variables vraies

Pourquoi 4 modèles pour un XOR triple ? - XOR = “nombre impair de variables vraies” - Pour 3 variables : 1 ou 3 vraies → 4 cas possibles - XOR binaire (a ^^ b) n’a que 2 modèles (1 vraie)

Astuce : La méthode toDnf() est utile pour visualiser les modèles d’une formule complexe.

Sémantique : Mondes possibles et satisfaction

Un monde possible (PossibleWorld) est une interpretation qui assigne une valeur de verite a chaque proposition. Une formule est satisfaite par un monde si elle est vraie dans ce monde.

# --- 2.1.1d Semantique : mondes possibles ---
if jvm_ready:
    # Creer un monde possible ou a=True et b=True
    world1 = PossibleWorld()
    world1.add(a)  # a est vrai
    world1.add(b)  # b est vrai
    # c et d sont implicitement faux (pas dans le monde)

    print(f"Monde possible w1 = {world1}")
    print(f"  (Propositions vraies: a, b)")

    # Verifier si le monde satisfait des formules
    f_test1 = pl_parser.parseFormula("a && !c")
    f_test2 = pl_parser.parseFormula("!b")
    f_test3 = pl_parser.parseFormula("a || c")

    print(f"\nSatisfaction dans w1:")
    print(f"  w1 |= 'a && !c' ? {world1.satisfies(JObject(f_test1, PlFormula_class))}")
    print(f"  w1 |= '!b'      ? {world1.satisfies(JObject(f_test2, PlFormula_class))}")
    print(f"  w1 |= 'a || c'  ? {world1.satisfies(JObject(f_test3, PlFormula_class))}")

    # Enumerer tous les modeles d'une formule
    print(f"\nModeles de 'a ^^ b ^^ c' (XOR):")
    models = list(formula_xor.getModels())
    for m in models:
        print(f"  {m}")
else:
    print("Cellule sautee : JVM Tweety non disponible")
Monde possible w1 = [a, b]
  (Propositions vraies: a, b)

Satisfaction dans w1:
  w1 |= 'a && !c' ? True
  w1 |= '!b'      ? False
  w1 |= 'a || c'  ? True

Modeles de 'a ^^ b ^^ c' (XOR):
  [a]
  [b]
  [a, b, c]
  [c]

Interpretation des mondes possibles et modèles

Monde possible w1 = [a, b]

Le monde w1 assigne : - a = True - b = True - c = False (implicite) - d = False (implicite)

Tests de satisfaction :

Formule w1 satisfait ? Explication
a && !c True a=T et c=F → T && T = T
!b False b=T → !T = F
a \|\| c True a=T → T || F = T

Modèles de a XOR b XOR c :

Les 4 modèles obtenus : 1. [a] → a=T, b=F, c=F → Nombre impair de T 2. [b] → a=F, b=T, c=F → Nombre impair de T 3. [c] → a=F, b=F, c=T → Nombre impair de T 4. [a,b,c] → a=T, b=T, c=T → Nombre impair de T

Sémantique XOR : Vrai si un nombre impair de variables sont vraies.

Distinction importante : - Monde possible : Une interpretation (assignation de verite) - Modèle : Un monde qui satisfait une formule donnee

Conversion DIMACS

Le format DIMACS CNF est le format standard pour les solveurs SAT. Tweety peut convertir une KB en DIMACS pour l’utiliser avec des solveurs externes.

p cnf <nb_variables> <nb_clauses>
<clause1> 0
<clause2> 0
...

Chaque variable est un entier positif, la negation est representee par un entier negatif.

# --- 2.1.1e Conversion DIMACS ---
if jvm_ready:
    # Creer une KB pour la conversion
    kb_dimacs = PlBeliefSet()
    kb_dimacs.add(pl_parser.parseFormula("a || b || c"))
    kb_dimacs.add(pl_parser.parseFormula("!a || b && d"))
    kb_dimacs.add(pl_parser.parseFormula("a"))
    kb_dimacs.add(pl_parser.parseFormula("!c"))

    print(f"KB originale: {kb_dimacs}")
    print(f"\nConversion en DIMACS CNF:")

    try:
        dimacs_lines = DimacsSatSolver.convertToDimacs(kb_dimacs)
        for line in dimacs_lines:
            print(f"  {str(line).strip()}")

        print("\nInterpretation:")
        print("  - 'p cnf 4 5' : 4 variables, 5 clauses")
        print("  - Variable 1 = a, 2 = b, 3 = c, 4 = d")
        print("  - '-1' signifie NOT a, '2' signifie b")
    except Exception as e:
        print(f"  Erreur conversion: {e}")
else:
    print("Cellule sautee : JVM Tweety non disponible")
KB originale: { a||b||c, a, !c, !a||(b&&d) }

Conversion en DIMACS CNF:
  p cnf 4 5
  1 2 3 0
  1 0
  -3 0
  -1 2 0
  -1 4 0

Interpretation:
  - 'p cnf 4 5' : 4 variables, 5 clauses
  - Variable 1 = a, 2 = b, 3 = c, 4 = d
  - '-1' signifie NOT a, '2' signifie b

Interpretation du format DIMACS

Sortie obtenue :

p cnf 4 5
1 2 3 0
1 0
-3 0
-1 2 0
-1 4 0

Decodage ligne par ligne :

Ligne DIMACS Signification Formule Tweety
p cnf 4 5 4 variables, 5 clauses (header)
1 2 3 0 Clause : 1 OR 2 OR 3 a \|\| b \|\| c
1 0 Clause : 1 a
-3 0 Clause : NOT 3 !c
-1 2 0 Clause : NOT 1 OR 2 !a \|\| b
-1 4 0 Clause : NOT 1 OR 4 !a \|\| d

Mapping variables : - Variable 1 → a - Variable 2 → b - Variable 3 → c - Variable 4 → d

Conversion formule → CNF : La formule !a || (b && d) devient 2 clauses : - !a || b → -1 2 0 - !a || d → -1 4 0

Utilite du DIMACS : - Format universel pour tous les solveurs SAT (CaDiCaL, Glucose, MiniSat, Z3) - Permet d’utiliser des solveurs externes sans wrapper Java - Standard de facto depuis les SAT Competitions (1990s)

2.1.2 Raisonnement Simple et Solveurs SAT (SAT4J interne)

Une fois les formules et bases définies, on peut effectuer des raisonnements :

  • Conséquence Logique (Query) : Déterminer si une formule \(\phi\) est une conséquence logique d’une base \(KB\) (\(KB \models \phi\)).
  • Satisfiabilité (SAT) : Déterminer si une base \(KB\) admet au moins un modèle (une assignation de vérité qui rend toutes les formules vraies).
  • Trouver un Modèle (Witness) : Si la base est satisfiable, trouver une assignation de vérité qui la satisfait.

Tweety propose : * SimplePlReasoner : Un raisonneur basique pour la conséquence logique, potentiellement lent. * SatSolver : Une interface pour les solveurs SAT. Sat4jSolver est une implémentation Java intégrée. SatSolver.setDefaultSolver(...) permet de choisir le solveur à utiliser globalement. * isSatisfiable(kb): Vérifie la satisfiabilité. * getWitness(kb): Retourne un PossibleWorld modèle si la KB est satisfiable, sinon None.

# --- 2.1.2 Logique Propositionnelle : Raisonnement et SAT4J ---
print("--- 2.1.2 Raisonnement PL et SAT4J ---")

if not jvm_ready:
    print("ERREUR: JVM non demarree.")
else:
    try:
        import jpype
        from jpype.types import JObject
        from java.util import Collection
        from org.tweetyproject.logics.pl.syntax import PlBeliefSet, PlFormula, Contradiction
        from org.tweetyproject.logics.pl.parser import PlParser
        from org.tweetyproject.logics.pl.reasoner import SimplePlReasoner
        from org.tweetyproject.logics.pl.sat import SatSolver, Sat4jSolver

        Collection_class = jpype.JClass("java.util.Collection")
        pl_parser_sat = PlParser()

        # === 1. SimplePlReasoner ===
        print("\n=== 1. SimplePlReasoner (Consequence Logique) ===")
        kb_str = "a || b || c\n!a || b\n!b || c"
        kb = pl_parser_sat.parseBeliefBase(kb_str)
        print(f"KB: {kb}")
        
        simple_reasoner = SimplePlReasoner()
        
        # Test: KB |= c ?
        # Explication: (!a||b) signifie a=>b, et (!b||c) signifie b=>c
        # Donc a => b => c, et avec (a||b||c), on deduit c
        query_c = pl_parser_sat.parseFormula("c")
        result_c = simple_reasoner.query(kb, query_c)
        print(f"\nKB |= c ? {result_c}")
        print("  Explication: a=>b et b=>c impliquent que c est toujours vrai")
        
        # Test: KB est-elle consistante ?
        query_false = Contradiction()
        result_cons = simple_reasoner.query(kb, query_false)
        print(f"\nKB |= contradiction ? {result_cons}")
        print("  False => la KB est consistante")

        # === 2. SAT4J Solver ===
        print("\n=== 2. SAT4J Solver (Satisfiabilite) ===")
        SatSolver.setDefaultSolver(Sat4jSolver())
        solver = SatSolver.getDefaultSolver()
        
        # Exemple SAT
        kb_sat = PlBeliefSet()
        kb_sat.add(pl_parser_sat.parseFormula("a || b"))
        kb_sat.add(pl_parser_sat.parseFormula("!a || c"))
        kb_sat.add(pl_parser_sat.parseFormula("b || !c"))
        print(f"\nKB SAT: {kb_sat}")
        print(f"  Satisfiable? {solver.isSatisfiable(kb_sat)}")
        
        # Exemple UNSAT
        kb_unsat = PlBeliefSet()
        kb_unsat.add(pl_parser_sat.parseFormula("a"))
        kb_unsat.add(pl_parser_sat.parseFormula("!a"))
        print(f"\nKB UNSAT (contradiction): {kb_unsat}")
        print(f"  Satisfiable? {solver.isSatisfiable(kb_unsat)}")

        # === 3. Enumeration des Modeles ===
        print("\n=== 3. Enumeration des Modeles ===")
        # Pour une formule simple, on peut enumerer tous les modeles
        formula_simple = pl_parser_sat.parseFormula("a ^^ b")  # XOR
        models = list(formula_simple.getModels())
        print(f"Formule: a XOR b")
        print(f"Nombre de modeles: {len(models)}")
        for m in models:
            print(f"  Modele: {m}")

    except Exception as e:
        print(f"Erreur: {e}")
        import traceback
        traceback.print_exc()
--- 2.1.2 Raisonnement PL et SAT4J ---

=== 1. SimplePlReasoner (Consequence Logique) ===
KB: { !a||b, !b||c, a||b||c }

KB |= c ? True
  Explication: a=>b et b=>c impliquent que c est toujours vrai

KB |= contradiction ? False
  False => la KB est consistante

=== 2. SAT4J Solver (Satisfiabilite) ===

KB SAT: { b||!c, a||b, !a||c }
  Satisfiable? True

KB UNSAT (contradiction): { !a, a }
  Satisfiable? False

=== 3. Enumeration des Modeles ===
Formule: a XOR b
Nombre de modeles: 2
  Modele: [a]
  Modele: [b]

Interpretation des résultats SAT4J

Exemple 1 : SimplePlReasoner (Consequence Logique)

Requête : KB |= c ?

Résultat : True

Explication detaillee :

KB = { a||b||c, !a||b, !b||c }

Reformulation en implications :
  !a||b  ≡  a => b
  !b||c  ≡  b => c

Donc: a => b => c

Avec a||b||c, on deduit que c est toujours vrai

Verification de consistance : - KB |= contradiction ? → False ✓ - La KB est consistante (au moins un modèle existe)

Exemple 2 : SAT4J Solver

KB Résultat Explication
{ a\|\|b, !a\|\|c, b\|\|!c } SAT Modèle possible : a=True, b=True, c=True
{ a, !a } UNSAT Contradiction directe

Exemple 3 : Enumeration des modèles

Formule : a XOR b - Modèle 1 : [a] (a=True, b=False) - Modèle 2 : [b] (a=False, b=True)

Remarque : XOR a exactement 2 modèles, comme attendu par la table de verite.

SAT4J vs solveurs modernes : SAT4J est portable (Java pur) mais ~10-20x plus lent que CaDiCaL/Glucose sur des problemes >1000 variables.

2.1.3 Solveurs SAT Modernes (pySAT / CaDiCaL)

Sat4j est un excellent solveur SAT en Java pur, mais pour des problèmes industriels complexes, les solveurs natifs modernes offrent des performances nettement supérieures.

Hiérarchie des Solveurs SAT (2024):

Solveur Origine Performance Caractéristique
CaDiCaL 1.9.5 A. Biere (TU Wien) ⭐⭐⭐⭐⭐ Champion SAT Competition, base de Kissat
CryptoMiniSat 5 M. Soos ⭐⭐⭐⭐ Spécialisé XOR (cryptographie)
Glucose 4.2 G. Audemard ⭐⭐⭐⭐ Apprentissage de lemmes agressif
MapleChrono V. Liang ⭐⭐⭐⭐ Backtracking chronologique
Lingeling A. Biere ⭐⭐⭐ Prédécesseur stable de CaDiCaL
Sat4j D. Le Berre ⭐⭐⭐ Java pur, portable

Pourquoi pySAT ?

# Installation: pip install python-sat
from pysat.solvers import Solver
from pysat.formula import CNF

# pySAT wraps native C/C++ solvers with Python interface
# - Same solver quality as standalone executables
# - Convenient Python API (no subprocess, no DIMACS files)
# - Incremental solving, assumptions, UNSAT cores

Comparaison typique (problème 10,000 variables): - Sat4j: ~10 secondes - CaDiCaL: ~0.5 secondes - Ratio: 20x plus rapide

# --- 2.1.3a Solveurs SAT Modernes: Comparaison sur Problemes Varies ---
print("--- 2.1.3a Solveurs SAT Modernes (pySAT / CaDiCaL) ---")

pysat_available = False
try:
    from pysat.solvers import Solver
    pysat_available = True
    print("pySAT installe - acces aux solveurs modernes!")
except ImportError:
    print("pySAT non installe. Installez avec: pip install python-sat")

if pysat_available:
    import time
    import random
    random.seed(42)
    
    def generate_pigeonhole(n_pigeons, n_holes):
        """Pigeonhole: n pigeons dans n-1 trous (UNSAT classique)"""
        clauses = []
        for i in range(1, n_pigeons + 1):
            clauses.append([(i-1)*n_holes + j for j in range(1, n_holes + 1)])
        for j in range(1, n_holes + 1):
            for i1 in range(1, n_pigeons + 1):
                for i2 in range(i1 + 1, n_pigeons + 1):
                    clauses.append([-(i1-1)*n_holes - j, -(i2-1)*n_holes - j])
        return clauses
    
    def generate_latin_square(n, seed=42):
        """Latin Square: chaque valeur une fois par ligne/colonne"""
        random.seed(seed)
        clauses = []
        def var(r, c, v): return r * n * n + c * n + v + 1
        for r in range(n):
            for c in range(n):
                clauses.append([var(r, c, v) for v in range(n)])
        for r in range(n):
            for c in range(n):
                for v1 in range(n):
                    for v2 in range(v1 + 1, n):
                        clauses.append([-var(r, c, v1), -var(r, c, v2)])
        for r in range(n):
            for v in range(n):
                for c1 in range(n):
                    for c2 in range(c1 + 1, n):
                        clauses.append([-var(r, c1, v), -var(r, c2, v)])
        for c in range(n):
            for v in range(n):
                for r1 in range(n):
                    for r2 in range(r1 + 1, n):
                        clauses.append([-var(r1, c, v), -var(r2, c, v)])
        return clauses
    
    def generate_queens(n):
        """N-Queens: placer n reines sans attaques"""
        clauses = []
        def var(r, c): return (r-1)*n + c
        for r in range(1, n+1):
            clauses.append([var(r, c) for c in range(1, n+1)])
        for r in range(1, n+1):
            for c1 in range(1, n+1):
                for c2 in range(c1+1, n+1):
                    clauses.append([-var(r, c1), -var(r, c2)])
        for c in range(1, n+1):
            for r1 in range(1, n+1):
                for r2 in range(r1+1, n+1):
                    clauses.append([-var(r1, c), -var(r2, c)])
        for r in range(1, n+1):
            for c in range(1, n+1):
                for d in range(1, n):
                    if r+d <= n and c+d <= n:
                        clauses.append([-var(r, c), -var(r+d, c+d)])
                    if r+d <= n and c-d >= 1:
                        clauses.append([-var(r, c), -var(r+d, c-d)])
        return clauses
    
    def benchmark(name, clauses, solvers=['cadical195', 'glucose42', 'minisat22']):
        n_vars = max(abs(lit) for clause in clauses for lit in clause) if clauses else 0
        print(f"\n--- {name} ---")
        print(f"  {n_vars} vars, {len(clauses)} clauses")
        results = {}
        for s in solvers:
            try:
                with Solver(name=s, bootstrap_with=clauses) as solver:
                    t0 = time.perf_counter()
                    res = solver.solve()
                    ms = (time.perf_counter() - t0) * 1000
                    results[s] = (res, ms)
                    print(f"    {s:12s}: {'SAT' if res else 'UNSAT':5s} {ms:8.2f}ms")
            except:
                print(f"    {s:12s}: N/A")
        return results
    
    # Warmup pour eviter le biais cold-start
    print("\n[Warmup des solveurs...]")
    warmup_cnf = [[1, 2], [-1, 2], [1, -2]]
    for s in ['cadical195', 'glucose42', 'minisat22']:
        with Solver(name=s, bootstrap_with=warmup_cnf) as solver:
            solver.solve()
    print("[Warmup termine]")
    
    all_results = {}

    # Test 1: Pigeonhole 9->8 (UNSAT) - CaDiCaL excelle sur UNSAT difficiles
    all_results['T1'] = benchmark("Test 1: Pigeonhole 9->8 (UNSAT crafted)",
                                   generate_pigeonhole(9, 8))

    # Test 2: Latin Square 13x13 (SAT) - Glucose excelle sur cette taille
    all_results['T2'] = benchmark("Test 2: Latin Square 13x13 (SAT combinatoire)",
                                   generate_latin_square(13))

    # Test 3: N-Queens 35 (SAT geometrique) - MiniSat excelle
    all_results['T3'] = benchmark("Test 3: 35-Queens (SAT geometrique)",
                                   generate_queens(35))

    # Comptage des victoires
    print("\n" + "="*50)
    wins = {s: 0 for s in ['cadical195', 'glucose42', 'minisat22']}
    for res in all_results.values():
        if res:
            best = min(res, key=lambda s: res[s][1])
            wins[best] += 1
    print(f"Victoires: CaDiCaL={wins['cadical195']}, Glucose={wins['glucose42']}, MiniSat={wins['minisat22']}")
    
    print("\nConclusion (narrateur data-driven, issu des victoires calculees):")
    _label = {'cadical195': 'CaDiCaL', 'glucose42': 'Glucose', 'minisat22': 'MiniSat'}
    _test_label = {'T1': 'Pigeonhole (UNSAT)', 'T2': 'Latin Square 13x13', 'T3': '35-Queens'}
    for _tk in ['T1', 'T2', 'T3']:
        _res = all_results.get(_tk)
        if _res:
            _best = min(_res, key=lambda s: _res[s][1])
            print(f"- {_test_label[_tk]}: {_label[_best]} le plus rapide ({_res[_best][1]:.2f}ms)")
    print(f"=> Victoires: CaDiCaL={wins['cadical195']}, Glucose={wins['glucose42']}, MiniSat={wins['minisat22']}")
else:
    print("Pour utiliser les solveurs modernes: pip install python-sat")
--- 2.1.3a Solveurs SAT Modernes (pySAT / CaDiCaL) ---
pySAT installe - acces aux solveurs modernes!

[Warmup des solveurs...]
[Warmup termine]

--- Test 1: Pigeonhole 9->8 (UNSAT crafted) ---
  72 vars, 297 clauses
    cadical195  : UNSAT   255.56ms
    glucose42   : UNSAT  2237.76ms
    minisat22   : UNSAT   321.71ms

--- Test 2: Latin Square 13x13 (SAT combinatoire) ---
  2197 vars, 39715 clauses
    cadical195  : SAT       1.56ms
    glucose42   : SAT       1.39ms
    minisat22   : SAT       1.57ms

--- Test 3: 35-Queens (SAT geometrique) ---
  1225 vars, 69055 clauses
    cadical195  : SAT      27.34ms
    glucose42   : SAT       2.82ms
    minisat22   : SAT       1.53ms

==================================================
Victoires: CaDiCaL=1, Glucose=1, MiniSat=1

Conclusion (narrateur data-driven, issu des victoires calculees):
- Pigeonhole (UNSAT): CaDiCaL le plus rapide (255.56ms)
- Latin Square 13x13: Glucose le plus rapide (1.39ms)
- 35-Queens: MiniSat le plus rapide (1.53ms)
=> Victoires: CaDiCaL=1, Glucose=1, MiniSat=1

Interpretation des benchmarks pySAT

Résultats obtenus (sortie de la cellule précédente) :

Test Vainqueur Remarque
Pigeonhole 9→8 (UNSAT) CaDiCaL UNSAT crafted difficile
Latin Square 13×13 (SAT) Glucose Apprentissage de lemmes
35-Queens (SAT) MiniSat Géométrie bien exploitée

Les temps absolus mesurés par chaque solveur sont le résultat live de la cellule de benchmark ci-dessus : ils varient d’une machine à l’autre (CPU, version Java/pySAT, charge), règle #9434 — la prose ne les fige pas. Ce qui est stable cross-machine, c’est le vainqueur de chaque instance et l’ordre de grandeur du rapport entre solveurs :

Instance Vainqueur Ordre de grandeur Diagnostic
Pigeonhole 9→8 (UNSAT, 72 var / 297 cl) CaDiCaL CaDiCaL ~6× plus rapide que Glucose UNSAT crafted : CaDiCaL domine
Latin Square 13×13 (SAT, 2197 var / 39715 cl) Glucose 3 solveurs quasi ex-aequo (quelques ms) SAT combinatoire petit : lemmes prime
35-Queens (SAT, 1225 var / 69055 cl) MiniSat MiniSat ~30× plus rapide que CaDiCaL SAT géométrique : heuristique spatiale

Victoires : CaDiCaL = 1, Glucose = 1, MiniSat = 1 (comptage automatique dans le code).

Analyse :

  1. Pigeonhole (UNSAT crafted) :
    • CaDiCaL domine nettement (~6× plus rapide que Glucose)
    • Glucose peine sur cet UNSAT difficile (plusieurs secondes)
    • MiniSat se place en intermédiaire
  2. Latin Square (SAT combinatoire) :
    • Les trois solveurs sont très proches (quelques ms) : instance petite, marge étroite
    • Glucose légèrement en tête grâce à son apprentissage de lemmes agressif
    • Structure régulière favorable aux heuristiques modernes
  3. N-Queens (SAT géométrique) :
    • MiniSat excelle ; CaDiCaL nettement en retrait (~30× plus lent)
    • Les contraintes géométriques jouent en faveur de l’heuristique MiniSat
    • Glucose également performant

Conclusion : - Aucun solveur universel : chaque problème a son champion - CaDiCaL : Robuste sur UNSAT difficiles et formules industrielles - Glucose : Excellent sur problèmes combinatoires avec structure - MiniSat : Rapide sur géométrie et contraintes spatiales

Honnêteté sur la mesure. Les temps produits par la cellule de benchmark ci-dessus sont un instantané d’une exécution sur une machine donnée — ils ne sont pas figés dans cette prose (règle #9434) : seuls les vainqueurs et les ordres de grandeur structurels sont reportés ici, car ce sont les seuls stables d’une machine à l’autre. À l’échelle de la milliseconde (Latin Square), le classement d’un test peut même basculer d’une exécution à l’autre — par exemple une exécution précédente donnait MiniSat vainqueur sur Latin Square (Glucose à 0 victoire). C’est précisément pour cela que la cellule de code calcule le vainqueur de chaque test (min(..., key=...)) et déduit sa conclusion du comptage de victoires plutôt que d’afficher des spécialités figées : la narration suit toujours les résultats réels, sans dérive.

Enumeration de solutions et integration Tweety

Au-dela de trouver UNE solution, pySAT permet d’enumerer toutes les solutions d’un problème SAT en ajoutant des clauses de blocage.

L’integration avec Tweety est simple: 1. Créer une KB avec PlParser et PlBeliefSet 2. Convertir en DIMACS avec DimacsSatSolver.convertToDimacs() 3. Parser le DIMACS pour pySAT 4. Resoudre avec CaDiCaL ou autre solveur moderne

# --- 2.1.3b Enumeration et Integration Tweety ---
print("--- 2.1.3b Enumeration de solutions et Integration Tweety ---")

if not pysat_available:
    print("pySAT non disponible - cellule sautee.")
else:
    # === Exemple 3: Enumeration de solutions ===
    print("\n--- Exemple 3: Enumeration des solutions ---")
    # Formule: a XOR b (exactement un des deux vrai)
    xor_clauses = [[1, 2], [-1, -2]]  # (a OR b) AND (NOT a OR NOT b)
    print(f"Clauses a XOR b: {xor_clauses}")

    solutions = []
    with Solver(name='cadical195', bootstrap_with=xor_clauses) as solver:
        while solver.solve():
            model = solver.get_model()
            solutions.append(model)
            solver.add_clause([-lit for lit in model])  # Clause de blocage

    print(f"  Nombre de solutions: {len(solutions)}")
    for i, sol in enumerate(solutions):
        print(f"    Solution {i+1}: a={sol[0]>0}, b={sol[1]>0}")

    # === Exemple 4: Integration avec Tweety ===
    if jvm_ready:
        print("\n--- Exemple 4: Integration Tweety -> pySAT ---")
        try:
            from org.tweetyproject.logics.pl.sat import DimacsSatSolver
            from org.tweetyproject.logics.pl.syntax import PlBeliefSet
            from org.tweetyproject.logics.pl.parser import PlParser

            # Creer une KB Tweety
            parser_sat = PlParser()
            kb_sat = PlBeliefSet()
            kb_sat.add(parser_sat.parseFormula("a || b || c"))
            kb_sat.add(parser_sat.parseFormula("!a || !b"))
            kb_sat.add(parser_sat.parseFormula("!b || !c"))
            kb_sat.add(parser_sat.parseFormula("a || c"))

            print(f"  KB Tweety: {kb_sat}")

            # Convertir en DIMACS
            dimacs_lines = [str(line) for line in DimacsSatSolver.convertToDimacs(kb_sat)]
            print("  Format DIMACS:")
            for line in dimacs_lines:
                print(f"    {line.strip()}")

            # Parser DIMACS pour pySAT
            cnf_pysat = []
            for line in dimacs_lines:
                line = line.strip()
                if line and not line.startswith(('c', 'p')):
                    lits = [int(x) for x in line.split() if x != '0']
                    if lits:
                        cnf_pysat.append(lits)

            # Resoudre avec CaDiCaL
            with Solver(name='cadical195', bootstrap_with=cnf_pysat) as solver:
                if solver.solve():
                    model = solver.get_model()
                    print(f"\n  Resultat CaDiCaL: SAT")
                    print(f"    Modele: {model[:4]}")  # 4 variables
                else:
                    print(f"\n  Resultat CaDiCaL: UNSAT")

        except Exception as e:
            print(f"  Erreur integration: {e}")

    print("\n==> pySAT est un excellent complement a Tweety pour le SAT.")
--- 2.1.3b Enumeration de solutions et Integration Tweety ---

--- Exemple 3: Enumeration des solutions ---
Clauses a XOR b: [[1, 2], [-1, -2]]
  Nombre de solutions: 2
    Solution 1: a=True, b=False
    Solution 2: a=False, b=True

--- Exemple 4: Integration Tweety -> pySAT ---
  KB Tweety: { !a||!b, !b||!c, a||c, a||b||c }
  Format DIMACS:
    p cnf 3 4
    -1 -2 0
    -2 -3 0
    1 3 0
    1 2 3 0

  Resultat CaDiCaL: SAT
    Modele: [1, -2, 3]

==> pySAT est un excellent complement a Tweety pour le SAT.

Interpretation : Enumeration et integration Tweety -> pySAT

Exemple 3 : Enumeration de solutions

Résultat : 2 solutions trouvees pour a XOR b - Solution 1 : a=True, b=False - Solution 2 : a=False, b=True

Technique de blocage :

while solver.solve():
    model = solver.get_model()
    solutions.append(model)
    solver.add_clause([-lit for lit in model])  # Bloque cette solution

La clause [-lit for lit in model] interdit exactement ce modèle.

Exemple 4 : Integration Tweety -> pySAT

Workflow complet : 1. Tweety : Créer KB avec PlParser et PlBeliefSet 2. Conversion : DimacsSatSolver.convertToDimacs(kb) → format DIMACS 3. Parsing : Extraire les clauses du DIMACS pour pySAT 4. Resolution : CaDiCaL trouve un modèle : [1, -2, 3] = a=True, b=False, c=True

Avantages de cette approche : - Tweety pour la modelisation (syntaxe intuitive) - pySAT pour la performance (solveurs C++ natifs) - Meilleur des deux mondes : expressivite + vitesse

Use case reel : Verification formelle, planning, configuration de produits

Exercice : Coloration de graphe avec SAT

Contexte

Un graphe non orienté à 4 sommets (A, B, C, D) a les arêtes suivantes : A-B, A-C, B-C, C-D. On souhaite colorier chaque sommet avec exactement une des 3 couleurs (Rouge, Vert, Bleu) de sorte que deux sommets adjacents n’aient jamais la même couleur.

Objectifs

  1. Modéliser ce problème en logique propositionnelle avec 12 variables X_couleur
  2. Construire la KB Tweety contenant les contraintes (au moins une couleur, au plus une couleur, exclusion arêtes)
  3. Résoudre avec Sat4jSolver et afficher la coloration trouvée
  4. Vérifier qu’une 2-coloration (2 couleurs seulement) est impossible sur ce graphe

Indices :

  • Variables : a_r, a_v, a_b, b_r, b_v, b_b, c_r, c_v, c_b, d_r, d_v, d_b
  • “Au moins une couleur” : a_r || a_v || a_b
  • “Au plus une couleur” : !(a_r && a_v) && !(a_r && a_b) && !(a_v && a_b)
  • “Pas même couleur sur arête A-B” : !(a_r && b_r) && !(a_v && b_v) && !(a_b && b_b)
# --- Exercice : Coloration de graphe (4 sommets, 3 couleurs) ---
# TODO etudiant : Construisez la KB avec les 12 variables et les contraintes
# Etape 1 : Creer les 12 propositions (a_r, a_v, a_b, b_r, ...)
# Etape 2 : Pour chaque sommet, ajouter "au moins une couleur" et "au plus une couleur"
# Etape 3 : Pour chaque arete, ajouter les contraintes d'exclusion de couleur
# Etape 4 : Resoudre avec Sat4jSolver et afficher la coloration
# Etape 5 : Retirer une couleur et verifier que le probleme devient UNSAT

print("Exercice a completer")
Exercice a completer

2.2 Logique du Premier Ordre (FOL)

La logique du premier ordre (First-Order Logic, FOL) étend la logique propositionnelle avec des prédicats, constantes, variables et quantificateurs.

Pourquoi FOL plutot que PL ?

Aspect Logique Propositionnelle Logique du Premier Ordre
Expressivité Faits simples Relations entre objets
Variables Non Oui (quantifiées)
Exemple pluie, parapluie Aime(jean, marie), forall X: (Humain(X) => Mortel(X))
Décidabilité Décidable (NP-complet) Semi-décidable

Composants de FOL:

Signature = Sorts + Constantes + Prédicats + Fonctions

Sorts (Types):        Humain, Animal, ...
Constantes:          jean, marie, fido (instances spécifiques)
Variables:           X, Y, Z (placeholders)
Prédicats:           Aime/2, Mortel/1, EstParentDe/2
Fonctions:           pere/1, mere/1 (retournent un terme)

Quantificateurs:
  - forall X: ...    "Pour tout X, ..."
  - exists X: ...    "Il existe X tel que ..."

Exemple classique - Syllogisme:

forall X: (Humain(X) => Mortel(X))   // Tous les humains sont mortels
Humain(socrate)                      // Socrate est humain
----------------------------------------
?- Mortel(socrate)                   // Donc: Socrate est mortel

Classes Tweety principales: * FolSignature: Définit les Sorts, Constants et Predicates * FolFormula: Formules incluant atomes, connecteurs et quantificateurs * FolParser: Parse les formules (nécessite une signature) * FolReasoner: Interface pour les prouveurs (EProver, SPASS, SimpleFolReasoner)

Limitation connue: SimpleFolReasoner peut causer des problèmes de heap space sur des requêtes complexes avec égalité. Pour un raisonnement FOL robuste, utilisez EProver.

Transition : De la Logique Propositionnelle a la Logique du Premier Ordre

Ce que nous avons vu en PL : - Propositions atomiques (a, b, rain, umbrella) - Connecteurs logiques (&&, ||, !, =>) - Mondes possibles et satisfiabilite - Solveurs SAT modernes (CaDiCaL, Glucose)

Limites de PL : - Impossible de representer “Tous les humains sont mortels” - Chaque instance necessite une proposition separee : mortel_socrate, mortel_platon, … - Pas de generalisation ni de quantification

Ce que FOL apporte : - Predicats : Relations entre objets (Aime(jean, marie)) - Quantificateurs : Generalisation (forall X: Humain(X) => Mortel(X)) - Variables : Placeholders pour les objets - Fonctions : Termes composes (pere(jean), age(X) + 1)

Exemple concret :

Representation Logique Propositionnelle Logique du Premier Ordre
“Socrate est mortel” mortel_socrate Mortel(socrate)
“Tous les humains sont mortels” mortel_socrate && mortel_platon && ... (infini!) forall X: (Humain(X) => Mortel(X))
“Il existe quelqu’un qui aime Marie” Impossible sans enumeration exists X: Aime(X, marie)

Prix a payer : - PL est decidable (SAT est NP-complet, mais resolvable) - FOL est semi-decidable (peut boucler indefiniment sur certaines requêtes) - Les solveurs FOL (EProver, SPASS) utilisent des heuristiques pour terminer en pratique

# --- 2.2.1 Imports et verification JVM pour FOL ---
print("--- 2.2.1 Imports FOL ---")

if not jvm_ready:
    print("ERREUR: JVM non demarree. Impossible de continuer cet exemple.")
    fol_imports_ok = False
else:
    print("JVM prete. Import des classes FOL...")
    fol_imports_ok = False
    try:
        # Imports Java necessaires
        import jpype
        from jpype.types import *
        from java.util import ArrayList, Collection
        import pathlib

        # Imports FOL Tweety
        from org.tweetyproject.logics.fol.syntax import FolFormula, FolSignature, FolBeliefSet, FolAtom
        from org.tweetyproject.logics.commons.syntax import Sort, Constant, Predicate, Variable
        from org.tweetyproject.logics.fol.parser import FolParser
        from org.tweetyproject.logics.fol.reasoner import FolReasoner, SimpleFolReasoner, EFOLReasoner

        # Verification des utilitaires
        if 'get_tool_path' not in globals() or 'EXTERNAL_TOOLS' not in globals():
            raise NameError("La fonction 'get_tool_path' ou 'EXTERNAL_TOOLS' n'est pas definie.")

        # Classes Java pour casting
        Collection_class = jpype.JClass("java.util.Collection")
        FolFormula_class = jpype.JClass("org.tweetyproject.logics.fol.syntax.FolFormula")
        
        print("Imports FOL/Commons reussis.")
        fol_imports_ok = True

    except ImportError as e:
        print(f"Erreur d'import pour FOL : {e}")
    except jpype.JException as e_java:
        print(f"Erreur Java generale FOL: {e_java.message()}")
    except Exception as e_gen:
        print(f"Erreur Python inattendue FOL: {e_gen}")
--- 2.2.1 Imports FOL ---
JVM prete. Import des classes FOL...
Imports FOL/Commons reussis.

Interpretation des imports FOL

Succes : Tous les imports FOL ont ete charges correctement.

Classes importees : - FolFormula, FolSignature, FolBeliefSet : Structures de base FOL - Sort, Constant, Predicate, Variable : Éléments de signature - FolParser : Parsing de formules textuelles - FolReasoner, SimpleFolReasoner, EFOLReasoner : Moteurs d’inference

Différence avec PL : - PL utilise PlFormula, PlSignature, PlBeliefSet - FOL ajoute le package commons.syntax pour les éléments partages (Sort, Constant, etc.) - La hiérarchie Tweety separe la syntaxe (formules) de la sémantique (raisonnement)

Astuce : Les classes *Reasoner sont des facades pour les solveurs externes (EProver, SPASS). Le pattern reste le même : reasoner.query(kb, formula) retourne True/False.

Creation de la Signature FOL

Une signature définit le vocabulaire de notre domaine : - Sorts : Les types d’objets (Person, City) - Constantes : Les individus (alice, bob, paris, london) - Predicats : Les relations entre objets (livesIn/2, mortal/1, isHappy/1)

Signature:
  Sorts:      Person, City
  Constantes: alice, bob : Person
              paris, london : City
  Predicats:  livesIn(Person, City)
              mortal(Person)
              isHappy(Person)
# --- 2.2.2 Creation de la Signature FOL ---
if fol_imports_ok:
    # Creer une signature avec predicats d'egalite integres
    sig_fol = FolSignature(True)
    
    # Definir les Sorts (types)
    sort_person = Sort("Person")
    sort_city = Sort("City")
    sig_fol.add(sort_person)
    sig_fol.add(sort_city)
    
    # Definir les Constantes
    alice = Constant("alice", sort_person)
    bob = Constant("bob", sort_person)
    paris = Constant("paris", sort_city)
    london = Constant("london", sort_city)
    sig_fol.add(alice)
    sig_fol.add(bob)
    sig_fol.add(paris)
    sig_fol.add(london)
    
    # Definir les Predicats
    livesIn_arity = ArrayList()
    livesIn_arity.add(sort_person)
    livesIn_arity.add(sort_city)
    livesIn = Predicate("livesIn", livesIn_arity)
    
    mortal_arity = ArrayList()
    mortal_arity.add(sort_person)
    mortal = Predicate("mortal", mortal_arity)
    
    isHappy_arity = ArrayList()
    isHappy_arity.add(sort_person)
    isHappy = Predicate("isHappy", isHappy_arity)
    
    sig_fol.add(livesIn)
    sig_fol.add(mortal)
    sig_fol.add(isHappy)
    
    print("Signature FOL creee:")
    print(sig_fol)
else:
    print("Imports FOL non disponibles - signature non creee.")
Signature FOL creee:
[_Any = {}, City = {london, paris}, Person = {alice, bob}], [isHappy(Person), ==(_Any,_Any), /==(_Any,_Any), livesIn(Person,City), mortal(Person)], []

Interpretation de la signature créée

Sortie obtenue : La signature contient 3 sorts, 5 predicats, et 0 fonctions.

Decomposition :

Sorts:
  - _Any (type universel)
  - City = {london, paris}
  - Person = {alice, bob}

Predicats:
  - isHappy(Person)
  - ==(Any, Any)      # Egalite (integree)
  - /==(Any, Any)     # Différence (integree)
  - livesIn(Person, City)
  - mortal(Person)

Pourquoi les types (Sorts) ? - Evitent les formules mal typees : livesIn(paris, alice) serait rejetee - Permettent l’optimisation des prouveurs (reduction de l’espace de recherche) - Utiles pour le typage statique des théories formelles

Note : Le type _Any est ajoute automatiquement pour les predicats d’egalite polymorphes.

Parsing de formules FOL

Le FolParser permet de parser des formules textuelles vers des objets FolFormula.

Syntaxe Tweety FOL :

Atome:        livesIn(alice, paris)
Egalite:      paris /== london    (différente de)
              paris == london     (egal a)
Connecteurs:  f1 && f2, f1 || f2, !f1, f1 => f2
Quantif.:     forall X: (Humain(X) => Mortel(X))
              exists X: Aime(X, marie)

Limitation Tweety 1.28: Le parsing de quantificateurs complexes peut echouer. Nous utilisons des faits atomiques simples pour cet exemple.

# --- 2.2.3 Parsing et Base de Croyances FOL ---
if fol_imports_ok:
    # Creer le parser avec notre signature
    parser_fol = FolParser()
    parser_fol.setSignature(sig_fol)
    
    # Creer la base de croyances
    kb_fol = FolBeliefSet()
    
    # Formules a parser (limitees aux faits atomiques pour eviter les bugs)
    formulas_to_test = [
        "livesIn(alice, paris)",   # Alice vit a Paris
        "livesIn(bob, london)",    # Bob vit a Londres
        "paris /== london",        # Paris et Londres sont differents
        "isHappy(alice)"           # Alice est heureuse
    ]
    
    print("Parsing des formules FOL dans la KB...")
    parsing_ok = True
    
    for f_str in formulas_to_test:
        try:
            formula_obj = parser_fol.parseFormula(f_str)
            kb_fol.add(JObject(formula_obj, FolFormula_class))
            print(f"  [OK] {f_str}")
        except jpype.JException as e_parse:
            print(f"  [ERREUR] {f_str}: {e_parse.message()}")
            parsing_ok = False
        except Exception as e_gen:
            print(f"  [ERREUR] {f_str}: {e_gen}")
            parsing_ok = False
    
    print(f"\nKB FOL contient {kb_fol.size()} formules.")
else:
    print("Imports FOL non disponibles - parsing ignore.")
Parsing des formules FOL dans la KB...
  [OK] livesIn(alice, paris)
  [OK] livesIn(bob, london)
  [OK] paris /== london
  [OK] isHappy(alice)

KB FOL contient 4 formules.

Interpretation du parsing FOL

Succes : Les 4 formules ont ete parsees correctement dans la KB.

Formules parsees : 1. livesIn(alice, paris) - Predicat binaire avec deux constantes typees 2. livesIn(bob, london) - Même predicat, instances différentes 3. paris /== london - Negation d’egalite (les deux villes sont distinctes) 4. isHappy(alice) - Predicat unaire

Différence avec PL : - En PL, alice_a_paris serait une proposition atomique (indivisible) - En FOL, livesIn(alice, paris) est un atome structure : - livesIn : predicat (relation) - alice, paris : termes (constantes typees) - Permet de raisonner sur les relations entre entites

Limitation du parsing simple : - Les formules ci-dessus sont des faits atomiques (ground atoms) - Pour des quantificateurs comme forall X: livesIn(X, paris), le parsing Tweety 1.28 peut echouer - Solution : construire manuellement avec ForallQuantifiedFormula ou utiliser EProver en mode TPTP

Raisonnement FOL : Choix du Raisonneur

Tweety propose plusieurs raisonneurs FOL :

Raisonneur Description Performance
SimpleFolReasoner Enumeration exhaustive Lent, heap space sur egalite
EFOLReasoner Utilise EProver externe Rapide, robuste
SPASSReasoner Utilise SPASS externe Rapide, moins portable

Recommandation: Utilisez EProver pour un raisonnement FOL robuste. SimpleFolReasoner est acceptable pour des KB très petites sans requêtes d’egalite.

# --- 2.2.4 Configuration du Raisonneur et Requetes ---
if fol_imports_ok and kb_fol.size() > 0:
    fol_reasoner = None
    
    # Tenter EProver si configure
    eprover_path_str = get_tool_path('EPROVER')
    
    if eprover_path_str:
        print(f"Configuration EProver: {eprover_path_str}")
        try:
            fol_reasoner = EFOLReasoner(JString(eprover_path_str))
            FolReasoner.setDefaultReasoner(fol_reasoner)
            print("  EProver configure comme raisonneur par defaut.")
        except Exception as e_eprover:
            print(f"  Erreur EProver: {e_eprover}")
            fol_reasoner = None
    
    # Fallback vers SimpleFolReasoner
    if not fol_reasoner:
        print("Utilisation de SimpleFolReasoner (fallback).")
        fol_reasoner = SimpleFolReasoner()
        FolReasoner.setDefaultReasoner(fol_reasoner)
    
    current_reasoner = FolReasoner.getDefaultReasoner()
    print(f"\nRaisonneur actif: {current_reasoner.getClass().getSimpleName()}")
else:
    print("KB vide ou imports manquants - raisonnement ignore.")
Configuration EProver: <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\EProver\eprover.exe
  EProver configure comme raisonneur par defaut.

Raisonneur actif: EFOLReasoner

Interpretation de la configuration du raisonneur

Résultat : EProver a ete configure avec succes comme raisonneur par defaut.

Comparaison des raisonneurs :

Critere SimpleFolReasoner EProver SPASS
Installation Integre Tweety Binaire externe Binaire externe
Performance Très lente Excellente Excellente
Robustesse Heap space frequents Robuste Robuste
Portabilite 100% (Java) Multi-OS Windows + Linux
Cas d’usage Tests basiques Production Logique modale

Astuce : EProver est le choix recommande pour tout raisonnement FOL au-dela des tests triviaux.

Exécution de Requêtes FOL

Testons l’inference logique sur notre base de connaissances : - livesIn(alice, paris) - Presente dans KB → True - livesIn(bob, paris) - Non deductible → False - isHappy(alice) - Presente dans KB → True - isHappy(bob) - Non deductible → False

Note: La requête paris == london est retiree car elle provoque un heap space avec SimpleFolReasoner (enumeration exhaustive de tous les mondes possibles).

# --- 2.2.5 Execution des Requetes ---
if fol_imports_ok and kb_fol.size() > 0:
    # Requetes simples (sans egalite de constantes)
    queries_fol_str = [
        "livesIn(alice, paris)",   # Devrait etre True
        "livesIn(bob, paris)",     # Devrait etre False
        "isHappy(alice)",          # Devrait etre True
        "isHappy(bob)",            # Devrait etre False/Unknown
    ]
    
    print("Resultats des requetes:")
    for q_str in queries_fol_str:
        try:
            query_formula = parser_fol.parseFormula(q_str)
            result = current_reasoner.query(kb_fol, JObject(query_formula, FolFormula_class))
            result_str = 'Unknown' if result is None else str(result)
            print(f"  {q_str} → {result_str}")
        except jpype.JException as e_query_java:
            print(f"  {q_str} → ERREUR JAVA: {e_query_java.message()}")
        except Exception as e_query_py:
            print(f"  {q_str} → ERREUR: {e_query_py}")
    
    print("\n[Note] Requete 'paris == london' retiree - voir section 2.2.1 pour EProver.")
else:
    print("Raisonnement FOL ignore (KB vide ou imports manquants).")
Resultats des requetes:
  livesIn(alice, paris) → True
  livesIn(bob, paris) → False
  isHappy(alice) → True
  isHappy(bob) → False

[Note] Requete 'paris == london' retiree - voir section 2.2.1 pour EProver.

Interpretation des résultats FOL

Analyse des résultats :

Requête Résultat Explication
livesIn(alice, paris) True Fait present dans la KB
livesIn(bob, paris) False Bob vit a Londres, pas Paris
isHappy(alice) True Fait present dans la KB
isHappy(bob) False Aucune information sur le bonheur de Bob (hypothese du monde clos)

Hypothese du monde clos (Closed World Assumption) : - Ce qui n’est pas prouvable est considere FAUX - Oppose a l’hypothese du monde ouvert (OWA) utilisee en Semantic Web - Typique des bases de données et systèmes experts

Différence FOL vs PL : - En PL, on manipule des propositions atomiques (a, b, c) - En FOL, on manipule des relations entre objets (livesIn(alice, paris)) - La FOL permet de factoriser avec des quantificateurs : forall X: (Humain(X) => Mortel(X))

Exercice : Modélisation FOL d’un domaine géographique

Contexte

Vous disposez d’une base de connaissances géographique simplifiée : - Paris et Lyon sont des villes françaises. Londres est une ville anglaise. - capitalOf(paris, france) et capitalOf(london, uk) sont des faits. - locatedIn(paris, europe) et locatedIn(lyon, europe) sont des faits.

Objectifs

  1. Créer une signature FOL avec les sorts City, Country, Region et les prédicats capitalOf/2, locatedIn/2, sameCountry/2
  2. Peupler la KB avec les faits ci-dessus
  3. Ajouter manuellement des règles : si deux villes sont dans le même pays (sameCountry), elles sont dans la même région
  4. Requêter : locatedIn(lyon, europe) est-il dérivable ? sameCountry(paris, lyon) ?

Indices :

  • Suivez le même pattern que la section 2.2 : créer FolSignature, ajouter sorts, constantes, prédicats
  • Utilisez FolParser avec la signature pour parser les faits
  • Pour les règles avec quantificateurs, utilisez EProver (SimpleFolReasoner ne les gère pas bien)
# --- Exercice : Modelisation FOL d'un domaine geographique ---
# TODO etudiant : Creez la signature, la KB et executez les requetes
# Etape 1 : Definir les sorts (City, Country, Region) et les constantes (paris, lyon, london, france, uk, europe)
# Etape 2 : Definir les predicats (capitalOf/2, locatedIn/2, sameCountry/2)
# Etape 3 : Peupler la KB avec les faits
# Etape 4 : Executer les requetes avec EProver ou SimpleFolReasoner

print("Exercice a completer")
Exercice a completer

2.2.6 Test EProver (Optionnel)

EProver est un prouveur automatique de theoremes pour la logique du premier ordre. Il est beaucoup plus efficace que SimpleFolReasoner pour les requêtes complexes, notamment celles impliquant l’egalite.

Note: EProver est auto-detecte depuis ext_tools/EProver/eprover.exe si present. Sinon, telechargez-le depuis eprover.org.

La cellule suivante teste EProver avec des requêtes qui feraient crasher SimpleFolReasoner (heap space).

# --- 2.2.6 Test EProver pour requetes FOL avancees ---
print("--- 2.2.6 Test EProver (Optionnel) ---")

if not jvm_ready:
    print("ERREUR: JVM non demarree.")
else:
    eprover_path = get_tool_path('EPROVER') if 'get_tool_path' in globals() else None
    
    if not eprover_path:
        print("EProver non configure. Ce test est saute.")
        print("Pour activer EProver, placez-le dans ext_tools/EProver/eprover.exe")
    else:
        print(f"EProver detecte: {eprover_path}")
        
        try:
            from org.tweetyproject.logics.fol.reasoner import EFOLReasoner, FolReasoner
            from org.tweetyproject.logics.fol.syntax import FolBeliefSet, FolSignature
            from org.tweetyproject.logics.fol.parser import FolParser
            from org.tweetyproject.logics.commons.syntax import Sort, Constant, Predicate
            from java.util import ArrayList
            from jpype.types import JObject, JString
            import jpype
            
            FolFormula_class = jpype.JClass("org.tweetyproject.logics.fol.syntax.FolFormula")
            
            # Creer un raisonneur EProver
            eprover_reasoner = EFOLReasoner(JString(eprover_path))
            print(f"Raisonneur cree: {eprover_reasoner.getClass().getSimpleName()}")
            
            # Signature simple pour le test
            sig = FolSignature(True)
            sort_thing = Sort("Thing")
            sig.add(sort_thing)
            
            a = Constant("a", sort_thing)
            b = Constant("b", sort_thing)
            sig.add(a)
            sig.add(b)
            
            # Predicats
            human_arity = ArrayList()
            human_arity.add(sort_thing)
            human = Predicate("human", human_arity)
            mortal = Predicate("mortal", human_arity)
            sig.add(human)
            sig.add(mortal)
            
            parser = FolParser()
            parser.setSignature(sig)
            
            kb = FolBeliefSet()
            for f_str in ["human(a)", "!mortal(a) || human(a)"]:
                f = parser.parseFormula(f_str)
                kb.add(JObject(f, FolFormula_class))
            
            print(f"\nKB: {kb.size()} formules")
            
            # Requetes avec EProver
            print("\nRequetes avec EProver:")
            for q_str in ["human(a)", "human(b)"]:
                q = parser.parseFormula(q_str)
                result = eprover_reasoner.query(kb, JObject(q, FolFormula_class))
                print(f"  {q_str}: {result}")
            
            print("\nEProver fonctionne correctement!")
            
        except Exception as e:
            print(f"Erreur: {e}")
--- 2.2.6 Test EProver (Optionnel) ---
EProver detecte: <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\EProver\eprover.exe
Raisonneur cree: EFOLReasoner

KB: 2 formules

Requetes avec EProver:
  human(a): True
  human(b): False

EProver fonctionne correctement!

Interpretation des résultats EProver

Observations : - EProver confirme human(a) car presente dans la KB - EProver refuse human(b) car aucune information sur b dans la KB (monde clos)

Avantages d’EProver : 1. Robustesse : Gere les quantificateurs complexes et l’egalite sans heap space 2. Performance : Champion CASC (Competition of Automated Theorem Provers) 3. Expressivite : Supporte FOL complete avec fonctions et egalite

Production : Pour des applications reelles, privilegiez EProver ou SPASS plutot que SimpleFolReasoner.

Exemple guide : Modelisation d’un problème de planification en logique propositionnelle

Contexte

Un enseignant doit planifier 3 cours (Maths, Info, Physique) sur 2 creneaux (Matin, Après-midi). Les contraintes sont : 1. Chaque cours doit etre assigne a exactement un creneau 2. Maths et Physique ne peuvent pas etre au même creneau (conflit de salle) 3. Info doit etre le matin

Objectifs

  1. Modeliser ce problème avec des propositions Tweety (Proposition, Negation, Conjunction, Disjunction)
  2. Construire la base de croyances (PlBeliefSet) contenant toutes les contraintes
  3. Utiliser le raisonneur SAT (Sat4jSolver ou pySAT) pour trouver une solution
  4. Verifier si la contrainte supplementaire “Physique le matin” est satisfiable avec les autres

Indices :

  • Utilisez 6 propositions : maths_am, maths_pm, info_am, info_pm, phys_am, phys_pm
  • “Exactement un creneau” = (x_am || x_pm) && !(x_am && x_pm)
  • “Pas au même creneau” = !(maths_am && phys_am) && !(maths_pm && phys_pm)
  • Reutilisez le pattern de parsing du notebook : parser_pl.parseFormula("...")
# --- Exemple guide : Planification en Logique Propositionnelle ---
# Solution complete : modelisation et resolution d'un probleme de planification

if jvm_ready:
    from org.tweetyproject.logics.pl.syntax import Proposition, PlBeliefSet, Negation, Conjunction, Disjunction
    from org.tweetyproject.logics.pl.sat import Sat4jSolver, SatSolver
    from org.tweetyproject.logics.pl.reasoner import SatReasoner

    parser = PlParser()
    p = parser.parseFormula

    kb = PlBeliefSet()

    for c in ("maths", "info", "phys"):
        kb.add(p(f"{c}_am || {c}_pm"))
        kb.add(Negation(p(f"{c}_am && {c}_pm")))

    kb.add(p("!(maths_am && phys_am)"))
    kb.add(p("!(maths_pm && phys_pm)"))

    kb.add(p("info_am"))  # Contrainte 3 : Info doit etre le matin

    SatSolver.setDefaultSolver(Sat4jSolver())
    solver = SatSolver.getDefaultSolver()

    if not solver.isSatisfiable(kb):
        print("Pas de solution.")
    else:
        # Extraction d'une affectation valide : pour chaque cours on tente le
        # creneau "matin" et on verifie via le solveur SAT qu'il reste
        # consistant avec les choix deja retenus ; sinon c'est l'apres-midi.
        # (L'extraction directe d'un temoin par Sat4j n'etait pas fiable ici :
        #  elle renvoyait une affectation ne satisfaisant pas la contrainte
        #  unitaire info_am, d'ou la reconstruction pas-a-pas ci-dessous.)
        choix = PlBeliefSet()
        for f in kb:
            choix.add(f)
        for nom, am, pm in (("Maths", "maths_am", "maths_pm"),
                            ("Info", "info_am", "info_pm"),
                            ("Physique", "phys_am", "phys_pm")):
            essai = PlBeliefSet()
            for g in choix:
                essai.add(g)
            essai.add(p(am))
            if solver.isSatisfiable(essai):
                choix.add(p(am))
                print(f"{nom:10} → matin")
            else:
                choix.add(p(pm))
                print(f"{nom:10} → après-midi")

    # Contrainte supplementaire : "Physique le matin" est-elle compatible ?
    kb.add(p("phys_am"))
    if solver.isSatisfiable(kb):
        print("\nPhysique le matin aussi → OK")
    else:
        print("\nPhysique le matin aussi → contradiction")
else:
    print("Exemple saute : JVM Tweety non disponible")
Maths      → matin
Info       → matin
Physique   → après-midi

Physique le matin aussi → OK

Exercice : Planification avec contraintes supplementaires

En vous basant sur l’exemple guide ci-dessus, etendez le problème de planification avec les contraintes suivantes :

  1. Ajoutez un 4e cours (Chimie) et un 3e creneau (Soir)
  2. Chimie ne peut pas etre le soir (contrainte de laboratoire)
  3. Maths et Chimie ne doivent pas etre au même creneau
  4. Trouvez une solution satisfaisant toutes les contraintes

Indices :

  • Utilisez 12 propositions : {maths,info,phys,chimie}_{am,pm,soir}
  • “Exactement un creneau” pour chaque cours
  • Reutilisez le pattern de construction KB de l’exemple guide
# --- Exercice : Planification etendue (4 cours, 3 creneaux) ---
# TODO etudiant : Construisez la KB avec les 12 propositions et les contraintes
# Etape 1 : Creer les propositions (maths_am, maths_pm, maths_soir, info_am, ...)
# Etape 2 : Ajouter les contraintes "exactement un creneau" pour chaque cours
# Etape 3 : Ajouter les contraintes d'exclusion (Chimie pas le soir, Maths != Chimie)
# Etape 4 : Resoudre avec Sat4jSolver et afficher l'emploi du temps

print("Exercice a completer")
Exercice a completer

Resume

Ce notebook a couvert: - Logique Propositionnelle (PL): Syntaxe, parsing, mondes possibles, SAT4J - Solveurs SAT Modernes: CaDiCaL, Glucose, CryptoMiniSat via pySAT (20x plus rapides que SAT4J) - Logique du Premier Ordre (FOL): Predicats, quantificateurs, signatures, EProver

Points cles: - Tweety excelle pour le parsing et la manipulation de formules logiques - pySAT complete Tweety avec des solveurs SAT haute performance - EProver est recommande pour le raisonnement FOL complexe (egalite, quantificateurs)

Prochaines étapes

Le notebook suivant explore les logiques plus avancees: Description Logic, Logique Modale, QBF.

Navigation: Tweety-1-Setup | Index | Tweety-3-Advanced-Logics

Retour au sommet