( quant [] (var X) x => quant Xs Ouvert (Fermé x) ) . ( quant [] x x => quant [] (Ouvert x) (Fermé x) ) . 
-terme objet. Le type l_terme est supposé augmenté d´un constructeur de variable libre, var de type string->l_terme, et d´un «quantificateur» de variable libre, libre de type string->(l_terme->l_terme)->l_terme (
ouvrir*).
Quantificateur.
n.m.
Le calcul des prédicats utilise les quantificateurs universel
(
)
et existentiel
(
).
Ce sont eux qui donnent une structure logique au domaine de discours.
La quantification universelle peut être vue comme un «et»
(
)
généralisé qui porte sur tout le domaine de discours,
tandis que la quantification existentielle serait un «ou»
(
)
généralisé.
Du point de vue de la démonstration,
il est fondamental de considérer les quantificateurs avec les
polarités* de leurs occurrences.
Les occurrences positives* de
et négatives* de
sont dites essentiellement universelles*,
alors que les occurrences négatives de et positives de
sont dites essentiellement existentielles*.
Les seules occurrences possibles de en Prolog sont négatives,
et donc essentiellement existentielles.
Par ailleurs, même si il n'y a pas toujours de syntaxe pour les noter,
les seules occurrences possibles de en Prolog sont positives.
Prolog ne permet donc que des quantifications essentiellement existentielles.
En Prolog,
peut avoir des occurrences positives et négatives,
et peut être noté en occurrence positive
et en certaines occurrences négatives
( types abstraits*).
Prolog permet donc d'utiliser les deux polarités de la quantification.
Quantification essentiellement existentielle.
n.f.
Quantification qui s'élimine en substituant à la variable quantifiée
un terme arbitraire.
En Prolog,
ces quantifications sont la quantification universelle au niveau des clauses
(
)
et la quantification existentielle au niveau des buts (
).
À ces deux quantifications correspondent des
règles de déduction* similaires.
La démonstration d'une formule quantifiée essentiellement existentiellement
réussit si et seulement si il existe un terme tel
qu'en le substituant à la variable quantifiée on obtient une formule prouvable.
Quantification essentiellement universelle.
n.f.
Quantification qui s'élimine en substituant à la variable quantifiée
une constante qui n'a d'occurrences ni dans la formule ni dans le programme.
En Prolog,
ces quantifications sont les quantifications universelles au niveau des buts
().
Dans le contexte du problème
d´unification d´ordre supérieur*,
on peut aussi considérer les -variables comme étant essentiellement
universellement quantifiées par des -abstractions*.
En effet,
à ces deux quantifications correspondent des
règles de déduction* similaires,
mais seulement si le principe d'extensionnalité des fonctions est admis.
On ajoute à ces deux quantifications la quantification universelle implicite
de toutes les constantes de la signature*.
Mais,
alors que les constantes de la signature sont considérées
universellement quantifiées avec la portée maximale
(c'est-à-dire à l'extérieur de toute autre quantification),
les -variables le sont avec la portée minimale
(c'est-à-dire à l'intérieur de toute autre quantification).
Un problème d'unification peut donc être schématisé comme suit :
,
où 
représente les quantifications universelles
qui encodent la signature,
celles-ci sont suivies
d'une combinaison quelconque de quantifications existentielles et universelles,
et le tout se termine par des quantifications universelles qui encodent des
-abstractions.
La notion de quantification essentiellement universelle
vient de l'observation par Miller que quantification universelle
et abstraction jouent le même rôle dans l'unification de
Prolog
[Miller 92].
L'intuition de cette notion est la suivante :
une abstraction 
dénote une fonction qui
à tout 
fait correspondre 
.
Convertir l'une en l'autre est un trait important de la programmation en
Prolog.
On peut considérer que la -abstraction est la forme
réifiée*
de la quantification universelle,
celle qui permet son stockage dans une structure de données.
Inversement,
la quantification universelle est la réflexion*
de la -abstraction dans la logique des programmes.
Elle est la structure de contrôle associée à la -abstraction.
Certaines quantifications universelles au niveau des buts ()
sont équivalentes à des quantifications existentielles au niveau des
clauses (
).
C'est l'idée de base d'une représentation des
types abstraits* en Prolog.
Question.
n.f.
(rel. but*)
(syn. requète*)
{