John Samuel
CPE Lyon
Année: 2024-2025
Courriel: john.samuel@cpe.fr
Les propositions dans la logique propositionnelle sont des déclarations qui peuvent être vraies (V) ou fausses (F). Supposons que nous ayons deux propositions simples : P, Q. Nous pouvons utiliser des connecteurs logiques pour créer des propositions plus complexes à partir de ces propositions simples.
Supposons que nous ayons quatre propositions simples : P, Q, R et S.
Avec ces propositions, nous pouvons définir des règles pour déterminer si une image représente la mer :
nous pouvons utiliser des opérateurs logiques pour combiner ces propositions et déterminer si l'image est celle de la mer :
Image de la mer : (P ET Q) OU (P ET R) OU (P ET S)
from propositional_logic import *
# définir les propositions
P = Proposition("L'eau est présente")
Q = Proposition("Il y a du sable")
R = Proposition("Des oiseaux marins sont présents")
S = Proposition("Des bateaux sont visibles")
# définir les propositions composées
rule1 = And(P, Q)
rule2 = And(P, R)
rule3 = And(P, S)
# définir la proposition principale
image_de_la_mer = Or(Or(rule1, rule2), rule3)
# évaluer des propositions
P.value = True
Q.value = True
R.value = False
S.value = False
print(image_de_la_mer.evaluate()) # Sortie: True
from propositional_logic import *
# Définir les propositions
A = Proposition("Des immeubles sont présents")
B = Proposition("Des voitures sont présentes")
C = Proposition("Des piétons sont présents")
D = Proposition("Des feux de circulation sont visibles")
# Définir les règles
ville = Or(Or(And(A, B), And(A, C)), And(A, D))
# Définir les valeurs des propositions
A.value = True
B.value = True
C.value = False
D.value = False
# Évaluer la valeur de la proposition "ville"
print(ville.evaluate()) # Sortie: True
from propositional_logic import *
# Définir les propositions
A = Proposition("L'utilisateur aime l'image actuelle")
B = Proposition("L'image actuelle est un portrait")
C = Proposition("L'image actuelle est une œuvre abstraite")
D = Proposition("L'utilisateur a aimé une œuvre similaire par le passé")
E = Proposition("L'image est en noir et blanc")
F = Proposition("L'image est en couleur")
G = Proposition("L'utilisateur préfère les œuvres d'art réalistes")
H = Proposition("L'image est une peinture réaliste")
I = Proposition("L'utilisateur a aimé les œuvres de cet artiste dans le passé")
J = Proposition("L'utilisateur n'aime pas les images très saturées")
K = Proposition("L'image a une saturation élevée")
# Définir les règles de recommandation
# 2. Si l'image est soit un portrait soit une œuvre abstraite (mais pas les deux),
# et que l'utilisateur a une préférence pour les œuvres réalistes, alors il n'aimera pas l'image actuelle.
recommandation_abstrait_ou_portrait = Implication(Xor(B, C), Not(G))
B.value = True
C.value = False
G.value = True
print(recommandation_abstrait_ou_portrait.evaluate())
# 6. Si l'utilisateur préfère les œuvres réalistes ou a aimé des œuvres similaires dans le passé,
# alors il n'aimera pas une œuvre abstraite (implication avec OU logique).
recommandation_non_abstrait = Implication(Or(G, D), Not(C))
G.value = True
D.value = False
C.value = False
print(recommandation_non_abstrait.evaluate())
Contrairement à la logique propositionnelle, qui traite uniquement de la vérité ou de la fausseté de propositions simples, la logique du premier ordre permet de représenter des informations structurées sur des objets et leurs relations. Voici quelques concepts clés de la logique du premier ordre :
Utilisez des parenthèses pour indiquer la priorité des opérations et la structure de la formule.
Utilisez des parenthèses pour indiquer la priorité des opérations et la structure de la formule.
Exemple :
Exemple :
Les fonctions sont utilisées pour attribuer des valeurs à des objets ou effectuer des opérations, tandis que les prédicats sont utilisés pour exprimer des relations ou des propriétés entre des objets et renvoient une valeur booléenne indiquant si la relation est vraie ou non.
Utilisons l'exemple des règles pour confirmer qu'une image représente effectivement une mer.
Utilisons l'exemple des règles pour confirmer qu'une image représente effectivement une mer.
Utilisons l'exemple des règles pour confirmer qu'une image représente effectivement une mer.
1. Pour déterminer si une image représente une scène de mer, nous pourrions utiliser une règle du type
∀x (ContientEau(x) ∧ ContientSable(x) => EstMer(x))
2. Nous pourrions également ajouter des règles spécifiques pour détecter des éléments spécifiques :
∀x (ContientBateaux(x) => EstPort(x))
∀x (ContientOiseauxMarins(x) => EstPlage(x))
3. Il existe au moins une image x telle que l'image contienne de l'eau et du sable.
∃x (ContientEau(x) ∧ ContientSable(x))
Z3 est un puissant solveur de contraintes développé par Microsoft Research, souvent utilisé pour la vérification formelle, le raisonnement logique, et d'autres tâches d'analyse symbolique. Il peut résoudre des équations et des inégalités, vérifier la satisfiabilité de formules logiques, et bien plus encore.
pip install z3-solver
from z3 import *
Pour créer des variables symboliques, vous utilisez les fonctions de Z3 comme Int(),
Real(), Bool(), etc. Cela crée deux variables entières x et
y.
from z3 import *
x = Int('x')
y = Int('y')
Vous pouvez maintenant formuler des contraintes logiques ou des équations en utilisant ces variables
constraint1 = x + y > 5
constraint2 = x - y < 3
Z3 utilise un solveur pour vérifier si ces contraintes peuvent être satisfaites :
solver = Solver()
solver.add(constraint1)
solver.add(constraint2)
Pour vérifier si les contraintes peuvent être satisfaites :
if solver.check() == sat:
print("Les contraintes sont satisfiables")
print(solver.model())
else:
print("Les contraintes ne sont pas satisfiables")
Si le solveur retourne `sat`, cela signifie qu'il existe une solution qui satisfait les contraintes, et vous pouvez afficher le modèle de solution avec `solver.model()`.
solver.check(): vérifie si les contraintes sont satisfiables.solver.model(): retourne une solution possible si les contraintes sont satisfiables.
solver.add(constraint): ajoute une ou plusieurs contraintes au solveur.Z3 est un outil très puissant pour résoudre des problèmes de logique et d'optimisation. Il est utilisé dans des domaines tels que la vérification de logiciels, la planification, et le raisonnement automatique. Une fois que vous vous familiarisez avec les bases, vous pouvez explorer des fonctionnalités plus avancées comme la quantification, les domaines spécifiques (bit-vectors, arrays), et la programmation modulaire.
Int (entiers), Real (nombres réels), Bool (booléens),
String (chaînes de caractères), etc.
DeclareSort, vous pouvez
créer des types complexes en combinant des types de base et des sorts définis par l'utilisateur.
And, Or, Not, et
Implies.
+, -, *, et /.
ForAll) : Utilisé pour exprimer des
propriétés qui doivent être vraies pour tous les éléments d'un certain type.Exists) : Utilisé pour exprimer qu'il
existe au moins un élément qui satisfait une certaine propriété.Solver est le cœur de Z3, utilisé
pour ajouter des contraintes et vérifier leur satisfaisabilité avec check().model() qui montre comment les constantes et variables doivent être assignées pour
satisfaire les contraintes.
Ajouter des Contraintes : Les assertions (add()) sont utilisées pour
introduire des contraintes dans le solver. Elles peuvent être des expressions booléennes ou des
équations.
Utilisé pour déclarer un nouveau type (ou sorte) dans le système de types de Z3. Cela permet de définir des objets qui ne correspondent pas à des types de base prédéfinis comme `Int`, `Bool`, etc.
Image = DeclareSort('Image')
Ici, Image est une nouvelle sorte qui peut représenter des images dans le modèle.
Utilisé pour déclarer des constantes d'un type spécifique. Cela signifie que vous créez une instance d'un objet de la sorte que vous avez définie.
x = Const('x', Image)
Ici, x est une constante qui est de type Image. Cela permet de représenter une
image particulière dans vos formules.
Utilisé pour déclarer des fonctions qui prennent des arguments et renvoient des valeurs. Ces fonctions peuvent être utilisées pour exprimer des relations entre des objets dans votre modèle.
ContientEau = Function('ContientEau', Image, BoolSort())
Ici, ContientEau est une fonction qui prend une constante de type Image et
renvoie un booléen (True ou False). Cela peut être utilisé pour vérifier si
une image contient de l'eau.
from z3 import *
# Créer un solver
solver = Solver()
# Définir une sorte pour les images
Image = DeclareSort('Image')
# Définir des fonctions pour vérifier le contenu d'une image
ContientEau = Function('ContientEau', Image, BoolSort())
ContientSable = Function('ContientSable', Image, BoolSort())
ContientBateaux = Function('ContientBateaux', Image, BoolSort())
ContientOiseauxMarins = Function('ContientOiseauxMarins', Image, BoolSort())
# Définir des relations pour les types d'images
EstMer = Function('EstMer', Image, BoolSort())
EstPort = Function('EstPort', Image, BoolSort())
EstPlage = Function('EstPlage', Image, BoolSort())
# Règles
# 1. Si une image contient de l'eau et du sable, alors c'est une mer
x = Const('x', Image)
solver.add(Implies(And(ContientEau(x), ContientSable(x)), EstMer(x)))
# 2. Si une image contient des bateaux, alors c'est un port
solver.add(Implies(ContientBateaux(x), EstPort(x)))
# 3. Si une image contient des oiseaux marins, alors c'est une plage
solver.add(Implies(ContientOiseauxMarins(x), EstPlage(x)))
# 4. Il existe au moins une image qui contient de l'eau et du sable
solver.add(Exists([x], And(ContientEau(x), ContientSable(x))))
# Exemple d'images à vérifier
img1 = Const('img1', Image)
img2 = Const('img2', Image)
# Définir des contenus pour img1 et img2
solver.add(ContientEau(img1) == True)
solver.add(ContientSable(img1) == True)
solver.add(ContientBateaux(img1) == False)
solver.add(ContientOiseauxMarins(img1) == False)
# Vérifier si les images respectent les règles
if solver.check() == sat:
print("Les images respectent les règles définies.")
else:
print("Les images ne respectent pas les règles définies.")
# Afficher les modèles (si satisfaisables)
print(solver.model())
La logique modale est une extension de la logique classique qui permet de raisonner sur la notion de "modalités", c'est-à-dire des catégories de propositions qui expriment des modalités ou des qualités spécifiques, telles que la nécessité, la possibilité, l'obligation, la croyance, etc
Opérateurs modaux : Les opérateurs modaux sont utilisés pour exprimer des modalités. Les deux opérateurs modaux les plus courants sont :
En logique modale, les termes "nécessaire", "contingent", "possible" et "impossible" sont utilisés pour décrire les modalités ou les qualités d'une proposition.
Exemple
Le raisonnement automatisé est un domaine de l'intelligence artificielle (IA) qui concerne la création de systèmes informatiques capables de tirer des conclusions logiques et de résoudre des problèmes de manière autonome, similaire à la manière dont les humains utilisent leur raisonnement pour résoudre des problèmes.
Le raisonnement automatisé peut être expliqué en utilisant différentes logiques, notamment la logique propositionnelle, la logique du premier ordre et la logique modale.
La représentation des connaissances joue un rôle central dans la manière dont les systèmes informatiques comprennent, raisonnent et interagissent avec le monde.
La représentation des connaissances désigne le processus de capture, de structuration et de stockage des informations et des connaissances de manière à les rendre utilisables par des systèmes informatiques. Cela implique de transformer des données brutes ou des concepts en une forme que les ordinateurs peuvent comprendre et exploiter pour résoudre des problèmes, prendre des décisions ou interagir avec les utilisateurs.
Les types de connaissances peuvent être classés en plusieurs catégories, notamment les connaissances déclaratives, les connaissances procédurales, les connaissances explicites et les connaissances tacites.
Dans la représentation des connaissances déclaratives, les faits, les informations et les connaissances sont exprimés sous forme de propositions logiques.
Graphes de Connaissances (Ontologies): Les ontologies sont des structures de données hiérarchiques qui organisent et hiérarchisent les connaissances en utilisant des concepts, des classes, des propriétés et des relations.
Les agents intelligents sont des entités logicielles ou matérielles capables de percevoir leur environnement, de prendre des décisions, et d'agir pour atteindre des objectifs spécifiques. Un agent intelligent est un système informatique ou une entité physique qui possède certaines caractéristiques clés :
Les agents intelligents peuvent être classés en différents types en fonction de leurs caractéristiques et de leurs capacités.
Dans l'apprentissage profond, le terme profond fait référence à la présence de multiples couches dans le réseau neuronal. Contrairement aux modèles plus simples, tels que les perceptrons monocouche, les réseaux profonds ont la capacité d'apprendre des représentations hiérarchiques complexes à partir de données brutes.