Imprimer

Introduction
Résumé 1.1 - Définition du langage (Tinhinen Meniche, Miguel Senovilla, Christian Abou hamad)

Objets
Une formule décrit une propriété qui parle d'objets (entiers, figures, ensembles...). Un symbole est une suite de caractères
spécifiques (ex: sqrt, +, *). L' arité est un entier naturel qui représente le nombre d'arguments associés à un symbole. Une
signature est un ensemble de symboles chacun associé à une arité. Un terme peut être une variable ou bien être formé d'un
symbole f d'arité n et d'une suite ordonnée de n termes t1, ..., tn. Les variables d'objet sont des symboles qui représentent des
objets arbitraires (ex : y+5).

Les formules atomiques sont des expressions qui représentent des formules vraies ou fausses et qui ne se décomposent
pas en formules plus simples. Elles peuvent être des symboles spéciaux (⊤ toujours vraie, ⊥ toujours fausse), ou bien des
symboles de prédicat associés à des objets. Un symbole de prédicat est une suite de caractères à laquelle on va attribuer un
sens (ex : x < y représente la relation "x strictement plus petit que y"). Un symbole de prédicat d'arité 0 représente à lui seul
une formule vraie ou fausse. Dans ce cas, on l'appelle variable propositionnelle.

Les formules complexes se construisent à l'aide de formules atomiques et connecteurs ou quantificateurs.

Partie propositionnelle négation ¬P

conjonction P∧Q
disjonction P∨Q
implication P⇒Q
Quantificateurs du premier ordre quantification universelle ∀x, P

quantification existentielle ∃x, P

On distingue deux catégories syntaxiques :
1. Les termes, construits à partir de variables objets et symboles de fonctions (comme 0 ou +) qui peuvent être des
constantes ou des fonctions d'arité au moins 1.
2. Les formules, construites à partir de variables propositionnelles et des symboles de prédicat.

La grammaire des termes et formules est la suivante avec C, F et FI les symboles de constantes, fonctions et fonctions
infixes, X, P, PI les symboles de prédicat, V les variables d'objet
term ::= V | C | F(list-terms) | term FI term | (term)
list-terms ::= term | list-terms, term
form ::= ⊤ | ⊥ | X | P(list-terms) | term PI term | (form)
| ¬form | form ∧ form | form ∨ form | form ⇒ form | ∀V, form | ∃V, form
La logique du premier ordre/calcul de prédicats est définie par sa signature (symboles de fonctions/prédicats) utilisant
uniquement les connecteurs et quantificateurs de la table.
Le calcul propositionnel/logique propositionnelle se réduit à l'utilisation de variables propositionnelles et connecteurs (mais
sans des quantificateurs!).

Traduire des énoncés en formule logique

1. Identifier les différentes entités mentionnées dans l'énoncé et leur faire correspondre un terme.
2. Identifier les formules atomiques en jeu, elles apparaîtront dans la formule finale.
3. Identifier les liens logiques entre formules atomiques (conjonctions, implications, etc).
4. Lier les variables à l'aide de quantificateurs.
5. Vérifier que la formule résultante représente la même vérité que l'énoncé.
 Imprimer

Introduction
Résumé 1.2 : Structure des formules (Hugo Barreiro, Adrien Challe, Safidy Vonintsoa)

1.2.1 Représentation des formules comme des arbres

Une formule peut se voir comme un arbre avec :

• noeuds internes –> des connecteurs logiques (binaires) ; les quantificateurs (∀x, Ǝx) et la négation (unitaires)
• feuilles –> les formules atomiques

➡ représenter les formules en machine / construire des fonctions sur les formules / raisonner sur les formules
1.2.2 Notations, règles de parenthésage

Règles de précédence = règles de priorités pour les connecteurs logiques

➡ lever toute ambiguïté / éviter le parenthésage inutile

Ordre de précédence : ㄱ puis Λ puis V puis ⇒ puis ∀ et Ǝ

⚠ Λ, V et ⇒ associent à droite donc P ⇒ Q ⇒ R se parenthèse P ⇒ (Q ⇒ R)

Remarque: dire que ¬ a une précédence plus forte que ∧ signifie que la formule ¬P∧Q doit se parenthéser en (¬P)∧Q. Donc,
les quantificateurs ∀ et Ǝ avec une précédence plus faible a une portée plus loin ∀x,(P ⇒Q) pour ∀x, P ⇒Q et non pas (∀x,
P)⇒Q.
➡ P ∧ R ∧ ¬Q ⇒ P ∨ Q ∧ R donne (P ∧ (R ∧ (¬Q))) ⇒ (P ∨ (Q ∧ R))

1.2.3 Variables libres, liées

Dans les formules ∀x, P et ∃x, P, la variable x est dite liée –> on peut changer le nom de manière cohérente dans P et le
quantificateur sans changer le sens de la formule
➡ ∀x, ∃y, x < y exprime la même propriété que ∀t, ∃u, t < u

Si x dans P mais pas dans une sous-expression de la forme ∀x, Q ou ∃x, Q, x est dite libre.

Déf - Variables libres, VI(P) : Soit une formule P et x une variable. On dit que x est libre dans la formule P et on écrira x ∈ VI(P)
si :
• P est une formule atomique R(t1, . . . , tn) et x apparaît dans l’un des termes ti
• P est une négation ¬A et x ∈ VI(A)
• P est une formule composée A ∧ B, A ∨ B, A ⇒ B et x ∈ VI(A) ou x ∈ VI(B)
• P est une formule quantifiée ∀y, A ou ∃y, A avec x ≠ y et x ∈ VI(A)

⚠ Une variable peut à la fois apparaître libre et liée dans une formule, ou bien apparaître liée dans plusieurs quantificateurs
comme y dans la formule 0 < x × y ∨ (∃y, x < y) ∧ (∃y, y + y < x)
Les variables libres représentent des paramètres de la formule et peuvent être remplacées par un terme plus complexe, on
parle de substitution (cf 1.5.3 pour la déf précise).

⚠ Attention au phénomène de capture lorsqu’on substitue une variable par un terme pouvant mener à un résultat erroné

Déf - Terme clos, formule close :

• Un terme qui ne contient pas de variables est appelé terme clos
• Une formule qui ne contient pas de variable libre est appelée formule close
 Imprimer

Introduction
Résumé 1-3 : Formules vraies (Jewin Cheng, Karim Rochd)

Les formules (closes) vraies :

Valeur de vérité = ensemble de booléens {V, F} noté aussi {1, 0}.

La formule atomique ⊥ est toujours fausse et la formule atomique ⊤ est toujours vraie.
Les tables suivantes rappellent les valeurs de vérité des connecteurs propositionnels en fonction des valeurs de vérité des
composants de la formule.

P Q ¬P P∧Q P∨Q P⇒Q P⇔ Q

V V F V V V V
V F F F V F F
F V V F V V F
F F V F F V V
La sémantique (sens de la formule) est différente de la syntaxe (forme).
Plusieurs formules peuvent avoir le même sens et des syntaxes différentes.
La même formule peut avoir différents sens, selon l’interprétation des symboles de la signature, donc on ne peut pas
connaitre la valeur de vérité d’une formule sans définir l’interprétation des symboles.
Les formules contiennent des symboles de fonctions et de prédicats qui correspondent à des primitives, de sens
indéterminé.

Une formule< est dite close< si elle ne contient pas de variable libres.

Une formule peut être

valide (tautologie) : vraie pour toutes les interprétations et toute valeur des variables.
insatisfiable : fausse pour toutes les interprétations et toute valeur des variables.
satisfiable : vraie pour au moins une interprétation, une valeur des variables.
P est valide ssi ¬P est insatisfiable ssi ¬P n’est pas satisfiable (ssi : si et seulement si)

Pour dire si une formule est vraie il faut expliciter dans quelle interprétation on se place (on utilise parfois le terme modèle) :
que représentent les symboles ?

Modélisation propositionnelle de problèmes :

Pour modéliser certains problèmes on introduit des variables propositionnelles correspondant à des situations dont on
cherche à déterminer si elles sont vraies ou fausses.
Les formules logiques représentent les contraintes associées au problème.

Formules avec quantificateurs :

Lorsqu’on a des quantificateurs, les variables représentent des inconnues dans un univers a priori indéterminé.

Un terme sans variable représente une valeur dans un domaine (ex. 2+3).

Un terme avec variable représente une valeur si on donne un environnement qui définit les valeurs des variables.

Une Interprétation explicite un domaine D, ensemble non vide (univers pour les objets), elle associe les symboles de fonction
à des fonctions sur le domaine et les symboles de prédicat à des relations entre objets.
 Imprimer

Introduction
Résumé 1.4 : Théories et modélisation (Lisa Ceresola, Eolyne Savary, Nadine Hage Chehade)

Définition d’une théorie :

• Signature : Ensemble de symboles de fonctions et de prédicats,
• Axiomes : ensemble de formules closes (sans variables libres)

–> C’est faire une modélisation de la logique d’un monde particulier.

NB : Une théorie peut être définie par un nombre infini d’axiomes.

Modèle d’une théorie :

Une interprétation de la signature d’une théorie telle que tous les axiomes de cette théorie sont vrais. Une théorie peut être :
• Incohérente : la théorie n’a pas de modèle
• Complète : pour toute proposition P, soit P est vraie dans tous les modèles, soit P est fausse dans tous les modèles
• Décidable : si pour toute proposition P, on peut décider si elle est conséquence ou non des axiomes (conséquence des
axiomes -> vraie dans tous les modèles)

Théorie de l’égalité :
Elle repose sur les axiomes de symétrie, réflexivité, transitivité, congruence et stabilité.
• Symétrie :
• Reflexivité :
• Transitivité :

• Congruence : pour toutes les fonctions f n-aire, on écrit un axiome de la forme

• Stabilité : pour chaque prédicat P n-aire, on écrit un axiome de la forme :

Modélisation : Modéliser une propriété consiste à concevoir une formule logique P sur la signature considérée.
• En logique propositionnelle :
- Signature : des formules propositionnelles (ie : sans quantificateurs, sans prédicats)
- Nécessite l’introduction de beaucoup de variables propositionnelles et d’axiomes
Attention à ne pas utiliser les quantificateurs ou les prédicats d’égalité !
Ex : ¬(Ba ∧ Bb) ∧ ¬(Ra ∧ Rb) où Ba, Bb, Ra, Rb sont des variables propositionnelles
• En logique du premier ordre :
- Signature : prédicats et fonctions,
- Utilisation de variables d’objets,
- Utilisation de quantificateurs
Ex : ∀a, b, ( (B(a) ∧ B(b)) ∨ (R(a) ∧ R(b)) ) ⇒ (a = b) où B et R sont des symboles de prédicats unaires, a et b sont des
variables d'objet

Exemple de modélisation en logique propositionnelle : Sudoku

• Variables propositionnelles : Xi,j,k est vrai si le chiffre k est présent à la case de coordonnées (i,j)
• Au plus un chiffre par case :
Pour i, j = 1, 2, …, 9, pour k = 1, 2, …, 9 : Xi,j,k ⇒ ¬Xi,j,1 ∧ … ∧ ¬Xi,j,(k-1) ∧ ¬ Xi,j,(k+1) ∧ … ∧ Xi,j,9
Ou de manière équivalente Pour i, j = 1, 2, …, 9, pour k = 1, 2, …, 9, pour n = k+1, …, 9 : ¬(Xi,j,k ∧ Xi,j,n)
• un chiffre apparait au moins une fois sur chaque ligne Pour k = 1, …, 9, pour i = 1, …, 9 : Xi,1,k ∨ … ∨ Xi,9,k
 Imprimer

Introduction
Résumé 1.5 : Définition récursive sur les formules (Moira Fruchaud, Alexis Gleyo)
La définition d'une fonction par des équations récursives sur la structure d'une formule associe une équation à chaque
construction possible de la formule. Le membre droit de l'équation peut être un appel récursif à des sous-formules de la
formule du membre de gauche.

Exemple :
• ℎ𝑡(𝑎𝑡𝑜𝑚) = 1
• ℎ𝑡(¬𝐴) = 1 + ℎ𝑡(𝐴)
• ℎ𝑡(𝐴 ∨ 𝐵) = 1 + 𝑚𝑎𝑥(ℎ𝑡(𝐴), ℎ𝑡(𝐵))
• ℎ𝑡(𝐴 ∧ 𝐵) = 1 + 𝑚𝑎𝑥(ℎ𝑡(𝐴), ℎ𝑡(𝐵))
• ℎ𝑡(𝐴 ⇒ 𝐵) = 1 + 𝑚𝑎𝑥(ℎ𝑡(𝐴), ℎ𝑡(𝐵))

où 𝐴 et 𝐵 représentent des formules quelconques et 𝑎𝑡𝑜𝑚 n'importe quelle formule atomique.

Si on traite des formules du calcul des prédicats (logique du premier ordre alors il faut ajouter des équations sur les
quantificateurs (mais pas en calcul propositionnel).

Schéma de récurrence pour les formules :

Afin de montrer que pour toute formule logique 𝑃 , Φ(𝑃 ) est vérifiée, il suffit de vérifier les points suivants :
• Φ(𝑝) est vérifiée lorsque 𝑝 est une formule atomique.
• Pour une formule 𝐴 quelconque, Φ(𝐴) implique Φ(¬𝐴)

• Pour des formules 𝐴 et 𝐵 quelconques, en supposant Φ(𝐴) et Φ(𝐵), on peut montrer Φ(𝐴 ∘ 𝐵) avec ∘ ∈ {∧, ∨, ⇒}
• Pour une formule 𝐴 quelconque, en supposant Φ(𝐴) , on peut montrer Φ(∀𝑥, 𝐴) et Φ(∃𝑥, 𝐴)

Exemple : Φ(𝑃 ) : 𝑛𝑏𝑎𝑡𝑜𝑚(𝑃 ) ≤ 1 + 𝑛𝑏𝑠𝑦𝑚𝑏𝑝(𝑃 )

Examen de chacun des cas possibles pour la formule 𝑃 :

Si 𝑃 est une formule atomique 𝑝, 𝑛𝑏𝑎𝑡𝑜𝑚(𝑝) = 1 et 𝑛𝑏𝑠𝑦𝑚𝑏𝑝(𝑝) = 0 donc Φ(𝑃 ) est vérifiée.
Si 𝑃 est une négation ¬𝐴 alors 𝑛𝑏𝑎𝑡𝑜𝑚(𝐴) ≤ 1 + 𝑛𝑏𝑠𝑦𝑚𝑏𝑝(𝐴) = 𝑛𝑏𝑠𝑦𝑚𝑏𝑝(¬𝐴) ≤ 1 + 𝑛𝑏𝑠𝑦𝑚𝑏𝑝(¬𝐴) donc Φ(¬𝐴)
est vérifiée.
Il faut faire de même avec toutes les autres constructions possibles.

Lorsque l'on substitue, il faut faire attention aux variables libres. Par exemple, la substitution ∀𝑦, 𝑅(𝑥, 𝑦)[𝑥 ← 𝑓(𝑥)] donne
𝑅(𝑓(𝑥), 𝑦), alors que ∀𝑥, 𝑅(𝑥, 𝑦)[𝑦 ← 𝑥] donne ∀𝑥′ , 𝑅(𝑥′ , 𝑥).
 Imprimer

Introduction
Résumé 2.1 : Interprétations et Vérité (Quentin Dilet, Danil Garmaev, Damien Ribeiro)

Définition : Une interprétation I d’une signature (F, R) [F l’ensemble des symboles de fonctions | R l’ensemble des symboles
de prédicat] est donné par :

• Un domaine D non vide appelé Domaine de l’interprétation.

• Pour chaque symbole de fonction d’arité n de F, une fonction à n variables de D qui donne un résultat à valeurs dans D.
• Pour chaque symbole de relation d’arité n de R, une relation n-aire sur D qui correspond à un ensemble de n-uplets de
valeurs dans D pour lesquels la relation est vraie dans l’interprétation.

Cas particulier : (symbole d’arité 0)

Dans le cas Propositionnel, il n’y a pas de symbole de fonction et il n’y a que des variables propositionnelles. L’interprétation
revient à fixer une valeur booléenne pour chacune des variables. Si n est le nombre de variables propositionnelles alors il y a
2n interprétations possibles.

Définition : Un environnement d’une interprétation I est une application (généralement notée ρ) qui associe une valeur du
domaine de l’interprétation à chaque variable qui apparaît dans les termes et les formules.

On note ρ+ {x|->d} l’environnement qui vaut d pour la variable x et ρ(y) pour toutes les variables y différentes de x.

Définition :

• Pour un terme t dans l’interprétation I et dans ρ, valI(ρ, t) est un élément de D: val I(ρ, x) = ρ(x) ; val I(ρ, f(t 1, …, t 2)) = f I(val I(ρ,
t1), …, valI(ρ, tn))
• Pour une formule dans l’interprétation I et dans ρ, valI(ρ, P) est une valeur de vérité dans {V; F} : val I(ρ, R(t 1, …, t n)) = si
RI(valI(ρ, t1),…, valI(ρ, tn)) alors V sinon F ; valI(ρ, A et B) = si valI(ρ, A) = V alors val I(ρ, B) sinon F

I, ρ |= A lorsque la formule A est vraie dans l’interprétation I et l’environnement ρ (val I(ρ, A) = V). La valeur de vérité d’une
formule close ne dépend pas de l’environnement, seulement de l’interprétation. On écrit alors val I(A).

Substitution et valeur de vérité : Soit une formule P, contenant une variable libre x et soit t un terme, ρ un environnement et I
une interprétation. S’il n’y a pas d’effets de capture créés par la substitution pour la formule P alors

valI(ρ, P[x<-t]) = valI(ρ+ {x|-> valI(ρ, t)}, P)

rappel - capture : lorsqu’une variable libre se retrouve par substitution sous un quantificateur qui porte sur une variable de
même nom (il faut alors modifier le nom de la variable liée qui n'est pas significatif).
 Imprimer

Introduction
Résumé 2.2 : Validité et satisfiabilité (Goncalves Vasconcelos Lucas, Lattari Rayane, Thierno Ka)

Ici I définit une interprétation, ρ un environnement et P une formule

- I, ρ ⊨ P veut dire que P est vrai dans ρ avec l'interprétation I
- P est valide ssi pour tout I,ρ, on a I,ρ ⊨ P. On le notera ⊨ P (On dira que P est une tautologie)
- P est satisfiable ssi il existe I,ρ, tels que I,ρ ⊨ P (On appellera I et ρ ici un modèle de la formule)
- P est insatisfiable ssi pour tous I,ρ, on a ¬(I,ρ ⊨ P)

Exemples:
1) P(x)∨¬P(x) est valide (peu importe P, ce sera toujours vrai ⊤) 2) Q(x,0) = 0 est satisfiable (dans le domaine des réels avec
pour Q la multiplication et l'égalité standards) 3) ¬P(x)∧P(x) est insatisfiable (ici peu importe P et x, ce sera toujours faux)

Pour un ensemble E de formules:

- E est valide ssi pour tout I,ρ, P∈E, on a I,ρ ⊨ P
- E est satisfiable ssi il existe I,ρ, tels que pour tout P∈E, on a I,ρ ⊨ P
- E est insatisfiable ssi pour tout I,ρ, il existe P∈E tel que ¬(I,ρ ⊨ P) On peut également l'écrire avec (I,ρ ⊭ P)

Exemples:
1) {} est valide (par défaut) 2) {P(x)∨¬P(x); ⊤ } est valide (les deux formules sont valides) 3) {P(x); Q(x)} est satisfiable (en
prenant une interprétation et un x ou P(x)∧Q(x) est vrai) 4) {⊥; P(x)∨¬P(x); ⊤} est insatisfiable (car ⊥ est insatisfiable peu
importe l'interprétation ou l'environnement)

Soit A une formule avec un variable libre x:

A valide ssi (∀x, A) valide, A satisfiable ssi (∃x, A ) satisfiable, A insatifiable ssi (∃x, A) insatisfiable
On peut appliquer récursivement ce raisonnement sur chaque variable libre pour tomber sur une formule sans variable libre
Exemples:
1) (∀z, z=z) ⇒ ∃y, x=y est valide (donc satisfiable) (ceci revient à dire pour tout x, y existe)
2) (∀z, z=z) ⇒ ∀y, ¬x=y est insatisfiable (peu importe x, si on prend y=x alors ¬y=x est faux donc ∀y, ¬x=y est faux)
3) x=4 est satisfiable (si on prend pour x la valeur de 4 et pour l'égalité, l'égalité du domaine )

2.2.2 Substitution et validité

Soit P une formule, E un ensemble de formules, x une variable et t un terme:

si P valide alors P[x<-t] valide
si E valide alors (E[x ←t] = {P [x ←t]|P ∈ E} par def) valide /!\ La réciproque est fausse

Exemple:
Avec x une variable libre, c une constante et Q un prédicat unaire:
- Q(x) ⇒Q(c) n'est pas valide (si x=1, c=2 et Q: y -> y=1)
- (Q(x) ⇒Q(c))[x ← c] = Q(c)⇒Q(c) est valide
Mais si P[x<-t] satisfiable alors P satisfiable (la réciproque est fausse aussi ici!!!)

Soit P et Q des formules et X une variable propositionnelle, le remplacement de X par Q dans P est une formule notée P [X
←Q] définie récursivement sur la structure de P .
X[X ←Q] = Q || P[X ←Q] = P (si P atomique et n'est pas X) || ¬A[X ←Q] = ¬(A[X ←Q])
(A◦ B)[X ←Q] = (A[X ←Q])◦ (B[X ←Q]) (avec ◦ un connecteur propositionnel)
(∀x, A)[X ←Q] = ∀x, (A[X ←Q]) (resp. (∃x, A)[X ←Q] = ∃x, (A[X ←Q])) (avec x non libre dans Q)
On a que: si P valide alors P[X ←Q] valide
 Imprimer

Résumé 2-3
Résumé 2.3 Conséquence logique, équivalence (Goncalves Vasconcelos Lucas, Lattari Rayane, Thierno Ka)

Conséquence logique:

• E⊨ A ssi pour tout I, ρ, si (I,ρ ⊨E) alors (I,ρ ⊨A)

• A ≡ B ssi A ⊨ B et B ⊨ A
• E insatisfiable ssi pour tout P, on a E⊨ P ssi E⊨ ⊥
• E ⊨ P ssi E ∪ {¬P } insatisfiable
• E, P ⊨ Q ssi E⊨P⇒Q

Soit x une variable et t un terme:

si E⊨P alors E[x←t]⊨P[x←t], de même pour l'équivalence

"si P valide alors P[x←Q] valide" est VRAI mais "si P[x←Q] valide alors P valide" est FAUX (x[x←⊤])

"si P satisfiable alors P[x←Q] satisfiable" est FAUX (x[x←⊥]) mais "si P[x←Q] satisfiable alors P satisfiable est VRAI
"si P insatisfiable alors P[x←Q] insatisfiable" est VRAI mais "si P[x←Q] insatisfiable alors P insatisfiable" est FAUX (x[x←⊥])

Soit E un ensemble de formule et A1,A2,B1,B2 des formules tel que : E,A1 ⊨B1 et E,A2 ⊨B2 on a donc:
E, ¬B1 ⊨ ¬A1 || E, A1 ∧ A2 ⊨ B1 ∧ B2 || E, A1 ∨ A2 ⊨ B1 ∨ B2 || E, B1 ⇒A2 ⊨ A1 ⇒B2

Si x n'est pas libre dans E:

E, (∀x,A1) ⊨ ∀x,B1 || E, (∃x,A1) ⊨ ∃x,B1

Algèbre de Boole:
P ∧ Q ≡ Q ∧ P || P ∨ Q ≡ Q ∨ P || (P ∧ Q) ∧ R ≡ P ∧ (Q ∧ R) || (P ∨ Q) ∨ R ≡ P ∨ (Q ∨ R)
P ∧ (Q ∨ R) ≡ (P ∧ Q) ∨ (P ∧ R) || P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R) || P ∧ ⊤ ≡ P || P ∨ ⊤ ≡ ⊤
P ∨ ⊥ ≡ P || P ∧ ⊥ ≡ ⊥ || ¬P ≡ P ⇒⊥ || P ⇒Q ≡ ¬P ∨ Q || P ⇔Q ≡ (P ⇒Q) ∧ (Q ⇒P ) ≡ (P ∧ Q) ∨ (¬P ∧ ¬Q)

Lois de Morgan:

¬⊥ ≡ ⊤ || ¬⊤ ≡ ⊥ || ¬¬P ≡ P || ¬(P ∧ Q) ≡ ¬P ∨ ¬Q || ¬(P ∨ Q) ≡ ¬P ∧ ¬Q

¬(P ⇒Q) ≡ P ∧ ¬Q || ¬∃x, P (x) ≡ ∀x, ¬P (x) || ¬∀x, P (x) ≡ ∃x, ¬P (x)
Définition: Une formule est dite en forme normale de négation si elle ne contient que les connecteurs logiques ∧, ∨, les
quantificateurs ∀, ∃ et que le symbole de négation n’apparait que devant une formule atomique R(t1, . . . , tn).

On peut inverser les quantificateurs (uniquement s'il sont les mêmes !!)
• ∀x, ∀y, R(x, y) ≡ ∀y, ∀x, R(x, y) || ∃x, ∃y, R(x, y) ≡ ∃y, ∃x, R(x, y)
• ∀x, (G(x) ∧ H(x)) ≡ (∀x, G(x)) ∧ (∀x, H(x))
• ∃x, (G(x) ∨ H(x)) ≡ (∃x, G(x)) ∨ (∃x, H(x))

Si x n'est pas une variable libre dans A:

• ∀x, A ≡∃x, A ≡ A
• ∀x, (A ∧G(x)) ≡ A ∧∀x, G(x) || ∀x, (A ∨ G(x)) ≡A ∨∀x, G(x)
• ∃x, (A ∧G(x))≡ A ∧∃x, G(x) || ∃x, (A ∨ G(x)) ≡A ∨∃x, G(x)
 Imprimer

Introduction
Résumé 2.4 Modèles particuliers (LEMATTRE Erwan, CHULILLA ARAGON Pablo, DUFOUR Ewen)

2.4.1 Modèles finis

Soit un domaine fini D={d1, ... , dn }.

On suppose que l'on a dans ce langage des termes sans variables {c1,...,c n } tels que val(c i ) = d i . Alors dans cette
interprétation, les formules suivantes sont vraies:

• (∀x,P)⇔(P[x←c1]∧...∧P[x←cn])
• (∃x,P)⇔(P[x←c1]∨...∨P[x←cn])

2.4.2 Modèles de Herbrand

Domaine de Herbrand d'un langage de signature (F,R): Ensemble noté T(F) des termes clos formés à partir de l'ensemble des
symboles du langage (dont les constantes).
Attention: Dans un domaine de Herbrand, les termes sont représentés comme des arbres. Par conséquent, 2 termes
syntaxiquement différents correspondront à 2 objets différents (même s'ils sont sémantiquement égaux dans certaines
théories).
Interprétation de Herbrand:
Interprétation construite sur le domaine de Herbrand dans laquelle on a, pour chaque symbole de fonction f d'arité
n, fH(t1,..., tn)=f(t1,...,tn), ti ∈ T(F)
Dans une interprétation de Herbrand, la valeur d'un terme clos est lui-même.

Base de Herbrand:
Ensemble des formules atomiques closes de la forme R(t1,..,tn) avec ti terme clos dans le domaine de Herbrand.
Formule universelle: formule de la forme ∀x1,... , xn, A avec A une formule sans quantificateurs.
Instance close d'une formule:
Soit A une formule ayant pour variable libres {x1, ..., xn}.
Une instance close de A est une formule de la forme A[x1←t1,...,xn←tn] avec ti ∈ T(F).
Théorème de Herbrand:
Soit B = ∀x1,... , xn, A une formule universelle close avec A sans quantificateurs.
B est satisfiable si et seulement si tout sous ensemble fini d'instances closes est satisfiable.
resp. B insatisfiable si il existe un sous ensemble fini d'instances closes de A qui soit insatisfiable.