Forme normale de Skolem
Un article de Wikipédia, l'encyclopédie libre.
 |
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
Une formule logique de premier ordre est sous forme normale de Skolem si sa forme normale prénexe contient uniquement des quantificateurs universels. Toute formule de premier ordre peut être convertie en forme normale de Skolem, tout en gardant sa satisfiabilité, via le procédé de skolémisation. La formule résultante de ce procédé n'est pas forcement équivalente à la formule d'origine.
Par exemple, la formule 
n'est pas sous forme normale de Skolem car elle contient un quantificateur existentiel. La skolémisation remplace y par f(x), où f est une nouvelle fonction et supprime le quantificateur 
. La formule résultante est 
.
