forme clausale et principe de résolution

Bonsoir,

J'ai une question qui concerne la résolution dans la logique des prédicat.

Quand on dit que B est une conséquence logique de A ( ou A démontre B) noté par, est-ce que ça veut dire que :
tout modèle de A est un modèle de B?

Si c'est le cas,

Si on veut démontrer que,

Soit E un ensemble de formules de la logique des prédicat et A une formule, E⊨A ça veut dire que:

Tout modèle commun des formules de E est un modèle de A ?

Pour appliquer le principe de résolution, il faut récrire les formules de E en forme clausale. Or, la forme clausale d'une formule n'est pas équivalente à celle-ci mais la formule n'est satisfiable que si et seulement sisa forme clausale l'est.

Si La propriété de satisfiabilité exprime qu'une formule a au moins un modèle, c-à-d,

A est satisfiable si et seulement si B est satisfiable veut dire que:

si A a au moins un modèle, B a au moins un modèle aussi (qui n'est pas forcément le même) et
si A n'a aucun modèle, B n'a aucun modèle aussi
et réciproquement.

Alors, comment la propriété de satifiablité est suffisante pour dire que l'on peut remplacer un ensemble de formules par l'ensemble des clauses issue de ces formules dans la preuve d'une conséquence logique?

J'espère que ma question est claire.

Merci d'avance,

Bonjour,

Je trouve que "Maxtimax" t'a très bien répondu.

J'aurais fait moins bien...

Si besoin, je te mets un lien pour consultation :

https://www.u-picardie.fr/~furst/docs/2-Resolution_Unification.pdf

Bon courage.

Bonjour,

Merci pour le lien, il contient un résumé très clair.

Je suis très reconnaissante pour Maxtimax de m'avoir aider, mais comme il ne connais pas le principe de résolution, j'ai encore quelques questions à éclairer.
C'est pour cela que j'ai essayé d'explorer d'autres sources.

Merci encore et bonne journée,