Bonjour,

je suis en train d'étudier la logique qui apparemment trouve une application en informatique.

Tout d'abord, une question de cours :
une clause est une disjonction de litéraux alors, on ne peut pas appliquer la procédure de Davis-Putnam sur :
(x et y) ou (x et y et z)  ?
On peut l'appliquer uniquement sur des formules du type :
(x ou y ou (non z)) et (x ou y) et (non z) par exemple.

Peut-on l'appliquer sur :
(x y) ou z ? (je pense que non car (x ) n'est pas une clause)

Soit M un ensemble de modèles m pour un langage L.
T une théorie, ensemble de formules.
J'ai remplacé le symbole de modèle par le symbole de preuve dans latex car il ne reconnait pas \models. (mais comme c'est équivalent, ça ne devrait pas gêner)

M M' M' M : Preuve :
Si M' alors pour tout m' M', m'
or M \subseteq M' donc un certain nombre de m' de M' sont dans M donc m'

T T' T T' : Preuve :
Si T alors pour tout m M, si m T alors m
or T T' donc si m T alors m T'
donc m T m T' et m
donc T'

D'après ce que j'ai compris, un modèle dans la logique des prédicats est un ensemble d'éléments : par exemple, l'ensemble des réels ou des complexes...etc

Mais dans la logique propositionnelle, est-ce qu'un modèle est bien un ensemble de litéraux qu'on pose vrai ou faux ?  

Merci pour votre aide