Cours 6 : Programmation logique

Programmation logique

Clause de Horn :

contient au plus un littéral positif.

Clause de Horn définie :

contient exactement un littéral positif.

Programme logique :

ensemble de clauses de Horn définies

Exemple :

Jeu de Nim :

• $G(X)$ : le premier joueur gagne avec $X$ allumettes

• $¬G(0)$
• $G(s(0))$
• $G(s(s(0))$
• $∀x, G(s(s(s(x)))) ⟺ ¬G(x)∨¬G(s(x))∨¬G(s(s(x)))$

s’écrit en programmation logique :

P(0)
G(s(0))
G(s(s(0))
G(s(s(s(x)))) :- P(s(s(x))) G(s(s(s(x)))) :- P(s(x))
G(s(s(s(x)))) :- P(x)

P(s(s(s(x)))) :- G(x), G(s(x)), G(s(s(x)))

où

• :- = $⟸$, i.e A :- B = $A∨¬B$
• , = $∧$

---

\[T_P(H) ≝ H ∪ \lbrace A𝜎∈Atomes clos \mid ∃ A∨¬B_1∨⋯ ∨¬B_n∈P \rbrace\]

où $H⊆\text{Atomes clos}$ tq $B_1 𝜎, ⋯, B_n 𝜎∈H$

$T_P$ : opérateur de conséquence immédiate.

Lemme :

$H \vDash P$ ssi $T_P(H)=H$

$⟹$ :

Soit $A𝜎∈T_P(H)$.

Il existe $A∨¬B_1∨⋯ ∨B_n ∈ P$, et $B_1 𝜎, ⋯, B_n 𝜎∈H$.

\[H \vDash (∀\overline{x}) A∨¬B_1∨⋯ ∨B_n ∈ P \\ H \vDash A𝜎∨¬B_1𝜎∨⋯ ∨B_n𝜎\]

donc

$H \vDash A𝜎$, et $A𝜎∈H$.

$⟸$ : idem

---

Lemme :

\[\bigcup\limits_{n≥0} T_P^n(∅)\]

est le plus petit modèle de Herbrand de $P$.

Preuve :

• l’ensemble des modèles de Hebrand ordonné par l’inclusion est un cpo.

• $T_P$ est continu : elle est montone et $T_P(\bigcup\limits_{n≥0} H_n) = \bigcup\limits_{n≥0} T_p(H_n)$ (où $(H_i)$ croît).

On conclut par le théorème de Kleene dans le cpo des parties d’atomes clos :

\[\bigcup\limits_{n≥0} T_P^n(∅)\]

est le plus petit point fixe de $T_P$

---

plus(zero,X,X).
plus(s(X),Y,s(Z)):- plus(X,Y,Z).