Définition (alphabet). L'alphabet de la logique des prédicats est constitué de
Notation.
Q dénote un quantificateur quelconque,
c-à-d ∀ ou ∃.
Les fonctions à 0 arguments sont appellées constantes et sont notés sans parenthèses
( a, b, ..., Socrate, ...).
Même chose pour les prédicats à 0 arguments, qui ne sont rien d'autre que des
variables propositionnelles.
Définition (terme). L'ensemble des termes est le plus petit ensemble de mots construits sur l'alphabet de la logique des prédicats tel que
Définition (formule).
Si p est un prédicat à n arguments et
t1,...,tn sont des termes alors
p(t1,...,tn) est une formule atomique.
L'ensemble FOR
des formules (ou formules bien formées) de la logique
des prédicats est alors défini de la même manière
qu'en logique propositionnelle,
en rajoutant une clause pour les quantificateurs :
Exemples de traduction d'énoncés en formules
Remarque sur les jeux de connecteurs primitifs
On reprend de la logique propositionnelle les notations pour les formules, la notion de sous-formule (en tenant compte des quantificateurs dans la définition) et les conventions pour économiser les parenthèses.
Définition (portée d'un quantificateur, variable libre).
Dans les formules (∀x A) et (∃x A) ,
la formule A est appellé la portée du quantificateur.
Une occurrence d'une variable est libre
si elle n'est dans la portée d'aucun quantificateur.
Sinon elle est liée.
Exemples
Définition (formule fermée, formule ouverte).
Une formule est fermée (ou close)
si elle ne contient pas de variables libres.
Sinon elle est ouverte.
Exemples
Définition (substitution de variables).
Une substitution de variables
est une application des variables dans les
termes qui est l'identité presque partout.
L'application d'une substitution à une expression E
est le résultat du remplacement simultanée de toutes les
occurrences libres des variables dans E
par leur terme associé.
Si E est une expression alors
(E)s est appelé une instance de E.
La composition de substitutions
est la composition de fonctions.
Notation.
Soit {x1 , ... , xn}
l'ensemble des variables
tel que s(x) est différent de x .
La substitution s est alors notée
s = {x1\t1 , ... , xn\tn}.
Exemples de substitutions
Définition (interprétation). Une interprétation I est constituée de
Définition (interprétation des termes). Une interprétation donnée I peut être étendue aux termes par
Définition (interprétation des formules).
Une interprétation I' est une
variante en x de I
si I' est identique à I sauf en x
(la seule différence entre I et I' est la valeur
qu'elles donnent à x).
N.B. : I et I' peuvent être identiques :
I est une variante de I en x .
Une interprétation donnée I peut être
étendue aux formules
par :
Comme en logique propositionnelle, I(A) = 1 est parfois noté |=I A , et nous dirons alors que I est un modèle de A.
Validité et satisfiabilité sont alors défini comme en logique propositionnelle, ainsi que la conséquence logique (Exemples).
Définition (axiomatique à la Hilbert). Les schémas d'axiome de la logique des prédicats sont ceux de la logique propositionnelle, plus
∀x A -> ((A){x\t})
(A){x\t} -> ∃x A
A A -> B
_____________
B
A -> B
______________
A -> (∀x B)
s'il n'y a pas d'occurrence libre de x dans A
et
A -> B
______________
(∃x A) -> B
s'il n'y a pas d'occurrence libre de x dans B
Même définition de preuve, de prouvabilité et de consistance qu'en logique propositionnelle (Exemples)
Remarque. Il est possible de définir également la déduction. Nous l'omettons ici, car elle est plus complexe que celle de la logique propositionnelle (les deux règles d'inférence pour les quantificateurs peuvent seulement être appliquées à des axiomes logiques, et non à des axiomes non-logiques et des formules déduites à partir de ceux-ci). De plus, cette notion peut être réduite à la validité, par un théorème de la déduction similaire à celui de la logique propositionnelle.
Même introduction et motivation qu'en logique propositionnelle
Théorème d'adéquation.
Si |- A alors |= A.
(même type de démonstration
qu'en logique propositionnelle)
Théorème de complétude.
Si |= A alors |- A.
(la démonstration est difficile)
Théorème (semi-décidabilité). La logique des prédicats est semi-décidable : il existe une procédure effective telle que pour toute formule A en entrée,
Remarque. Étant donné les théorèmes d'adéquation et de complétude, les propriétés qui suivent peuvent être formulées et en termes de prouvabilité (avec |-) et en termes de validité (avec |=).
Définition (forme normale prénexe).
Une formule A est en forme normale prénexe
si elle est de la forme
Qx1 ... Qxn B ,
où B est une formule sans quantificateurs.
La suite des quantificateurs est appellée préfixe,
et B est appellée matrice.
Exemples
Théorème.
Pour toute entrée A, l'algorithme
de mise en forme normale prénexe s'arrête.
Il retourne une formule en forme normale prénexe
équivalente à l'entrée.
(la démonstration utilise que les équivalences sont valides
- en particulier ceux de la dernière étape reposent sur le fait que
grâce au renommage de l'étape précédente
toutes les occurrences de x sont dans la portée de Q x - ,
ainsi que le
théorème de la substitution des équivalents :
les remplacements effectués par l'algorithme
correspondent à des équivalences prouvables).
Définition (forme normale de Skolem).
Une formule est en forme normale de Skolem
si elle est
en forme normale prénexe et
ne contient pas de quantificateur existentiel.
Remarque. Si n = 0 on substitue par une constante.
Théorème.
Pour toute formule d'entrée A, l'algorithme
de mise en forme normale de Skolem s'arrête.
Il retourne une formule A' en forme normale de Skolem telle que
A est satisfiable ssi A' est satisfiable.
(la démonstration utilise que toutes les étapes préservent la satisfiabilité ;
notons que la mise en forme normale prénexe
préserve même l'équivalence logique)
Remarque. Dualement, on obtient l'équivalence de validité si on remplace les variables quantifiées universellement par une fonction des variables quantifiées existentiellement.
Définition (forme normale clausale).
Une formule est en forme normale clausale si elle est
en forme normale de Skolem,
fermée
et sa matrice est en
forme normale conjonctive propositionnelle.
Exemples
Notation.
Comme toute variable est quantifiée universellement, nous pouvons éliminer le préfixe.
Avec les mêmes
définitions de littéral et clause
qu'en logique propositionnelle
nous pouvons appliquer la même convention notationnelle :
une formule est représentée par un ensemble d'ensembles de littéraux.
Théorème.
Pour toute entrée A, l'algorithme
de mise en forme normale clausale s'arrête.
Il retourne une formule A' en forme normale clausale telle que
A est satisfiable ssi A' est satisfiable.
(la démonstration est un corollaire du
théorème pour la forme normale de Skolem et du
théorème pour la forme normale conjonctive
de la logique propositionnelle)
Définition (unifieur).
Une substitution s
unifie deux termes
si elle les rend identiques :
s unifie t et t' si
(t)s = (t')s.
Un unifieur d'un ensemble fini d'équations entre termes
E = {t1=t'1 , ... , tn=t'n}
est une substitution qui unifie les deux termes de chaque équation.
Exemples
Définition (unifieur le plus général).
Soient t et t' deux termes, et
s un unifieur de t et t'.
s est un unifieur le plus général (upg) si
pour tout unifieur s' de t et t'
il existe une substitution s'' telle que
s' = s'' o s.
Exemples
Théorème. Si un ensemble d'équations entre termes est unifiable alors il existe un unique upg s (à un renommage de variables près).
Définition (équations résolues).
Un ensemble d'équations
E est résolu si
Soit
Théorème. Si un ensemble de termes est unifiable alors l'algorithme calcule leur upg, sinon il s'arrête sur échec.
Définition (facteur).
Soit C une
clause telle que
Alors (C)s
est un facteur de C.
ou bien C =
{~p(t1,...,tn),~p(t'1,...,t'n)}
U
D ,
et
Exemples
Définition (réfutation). Une réfutation des clauses C1,...,Cm est une liste finie de clauses (D1, ... ,Dn) telle que
Théorème. Soit A une formule en forme normale clausale, et soient x1,...,xm les variables libres de A. Alors ∀x1 ... ∀xn A est insatisfiable ssi il existe une réfutation de l'ensemble de clauses associé à A.
Corollaire. Pour savoir si une formule donnée A est valide en logique des prédicats, il suffit de
N.B. : Il est possible qu'aucun des deux conditions d'arrêt soit atteinte (voir p.ex. le dernier des exemples). La résolution est donc un exemple de procédure de semi-décision pour la logique des prédicats.
Définition (réfutation linéaire). Une réfutation est linéaire si
Théorème. Soit E un ensemble de clauses. Si il existe une réfutation de E alors il existe une réfutation linéaire de E.
Définition (clause de Horn). Une clause de Horn est une clause avec au plus un littéral positif.
Théorème. Soit E un ensemble de clauses de Horn. Si il existe une réfutation de E alors il existe une réfutation linéaire de E où la règle de factorisation n'est pas utilisée.
Définition (fait, règle, programme logique, question).
Un fait
est un littéral positif.
Une règle
est une clause avec un littéral positif et au moins un littéral négatif
(elle est donc de la forme
{p, ~p1, ..., ~pn},
avec n > 0)
Un programme logique
est une liste de faits et règles.
Une question
est une clause sans littéral positif.
Exemples
Définition (réponse).
Soit P un programme logique, et soit C une question.
Alors une substitution s est une réponse
ssi
P
U
{(C)s} est insatisfiable.
Exemples