Une transformation syntaxique qui élimine les quantificateurs existentiels en introduisant des fonctions ou constantes de Skolem, produisant une formule équisatisfiable où les existentiels sont supprimés, souvent en vue d'obtenir la forme clausale pour le raisonnement automatique.

Principe

Remplacer des variables quantifiées existentiellement par de nouvelles fonctions de Skolem dont les arguments sont les variables universelles en portée du quantificateur existentiel ; cela préserve la satisfaisabilité (mais pas l'équivalence logique) et fournit des formules adaptées à la résolution.

Démonstration

À partir de ∀x ∃y P(x,y) transformer en ∀x P(x, f(x)) en introduisant une fonction de Skolem f ; les modèles satisfaisables de l'original correspondent aux modèles de la forme skolemienne avec une interprétation appropriée de f.

Mauvaise application

Considérer la skolemisation comme préservant l'équivalence plutôt que la seule satisfaisabilité conduit à des substitutions non valides dans des contextes nécessitant l'équivalence logique (par ex. lors d'extractions de conséquences déductives plutôt que de vérifications de satisfaisabilité).

Conséquence

La skolemisation permet des procédures de preuve mécanisées (génération de clauses, résolution) en supprimant les quantificateurs existentiels et en produisant une forme apte à l'unification et à la recherche automatique ; elle simplifie la gestion des témoins tout en pouvant masquer le contenu constructif.

Inversion

L'inverse consiste à réintroduire des quantificateurs existentiels ou des témoins explicitement (termes témoins ou constantes de Skolem constructives) pour retrouver l'équivalence et l'information constructive ; cela exige souvent des informations supplémentaires ou une preuve d'existence.

Limite

Garantit l'équisatisfiabilité pour les formules du premier ordre lorsqu'elle est appliquée correctement, mais ne préserve pas en général la validité ni la direction d'entaillement ; elle n'est pas directement applicable sans adaptation dans certains cadres d'ordre supérieur ou constructifs.

Tension sémantique

Tension avec les interprétations constructives : la skolemisation est classique et modèle-théorique (préservant la satisfaisabilité) et s'oppose aux besoins constructifs de produire des témoins explicites ou de maintenir des affirmations d'existence démontrables.

Synthèse

La skolemisation est une réécriture syntaxique préservant les modèles qui remplace les quantificateurs existentiels par des symboles de fonction nouveaux dépendant des variables universelles environnantes, échangeant l'équivalence logique contre l'équisatisfiabilité pour faciliter le raisonnement automatique basé sur des clauses.