-terme objet de constructeurs de variable libre, var, aux occurrences des variables libres désignées comme telles par un «quantificateur» de variable libre, libre. C´est l´opération inverse de quant*, mais elle peut être programmée beaucoup plus simplement en utilisant la 
-réduction du métalangage. Cependant, la programmation de ouvrir est mono-directionnelle (mode (ouvrir + ? ?)), alors que celle de quant est bi-directionnelle (modes (quant + + ?) et (quant ? ? +)).
o.
Type des valeurs de vérité.
Dans les écrits logiques classiques
(par exemple,
Church [Church 40]),
le type o s'oppose au type i qui distingue les individus,
les termes.
En Prolog,
le type i est remplacé par des types définis dans des bibliothèques ou par
l'utilisateur.
Ils fournissent une classification plus fine des individus.
Ce -terme* contient un seul -rédex* (lui-même)
et se -réduit* en lui même.
Il est l'archétype des
-termes sans forme normale.
Ordre supérieur.
n.m.
(ant. premier ordre*)
Désigne une structure hiérarchique où on
peut avoir à certains niveaux des quantifications qui ont pour domaine des
objets de niveau supérieur ou égal.
Par exemple,
une logique d'ordre supérieur pourra soit avoir des quantifications dans
les termes (-abstraction*),
soit avoir des formules quantifiées sur les formules,
soit avoir les deux.
Un langage de programmation fonctionnel d'ordre supérieur
pourra avoir des fonctions de fonctions.
On voit que l'extension à l'ordre supérieur d'une logique de premier
ordre peut prendre plusieurs voies.
Prolog met en 
uvre la troisième :
-abstraction dans les termes et quantification sur les formules
(voir par exemple les buts faux* et vrai*
).
.
.