1 0 
) où 
est la transformée de Fourier discrète d´un vecteur 
de longueur 
, et (calc 
) si et seulement si 
, où 
est la -ième racine de l´unité.
Fait.
n.m.
(rel. clause*)
Clause constituée d'un
littéral* positif*.
On l'appelle aussi clause unitaire.
En termes de base de données,
un fait est un enregistrement élémentaire.
Faux.
n.m.
(
vrai*)
Flexible.
adj.
(ant. rigide*)
Forme normale.
n.f.
Le calcul des prédicat et le 
-calcul introduisent chacun une
relation d'équivalence et donc une notion de formules ou de termes qu'on va
sélectionner sur des critères syntaxiques
pour représenter une classe.
Les formes normales étudiées
sont souvent choisies comme des structures de données pour décrire des
algorithmes.
Employée seule, l'expression «forme normale» désigne la
forme 
-normale*.
Forme -normale.
n.f.
Terme du -calcul*
qui ne contient pas de -rédex*.
Que ce soit pour la programmation fonctionnelle ou pour Prolog,
on ne calcule pratiquement jamais de forme -normale.
En effet,
le but d'un tel calcul est le plus souvent d'être capable de comparer
deux -termes,
ou de simplifier un -terme pour le visualiser.
Il faut noter au passage
que la -réduction* peut avoir l'effet
inverse d'une simplification,
mais que cela n'arrive pas trop souvent.
Les langages de programmation fonctionnelle,
même ceux qui sont d'ordre supérieur,
ne comparent pas les fonctions et n'affichent pas leur corps.
Pour l'utilisateur de tels langages les fonctions calculées restent des
«boîtes noires».
D'un point de vue procédural,
tout ce résume dans le slogan «ne pas réduire sous les lambdas».
Prolog compare les fonctions
( unification d´ordre supérieur*),
mais il le fait par le biais d'étapes élémentaires qui ne nécessitent
que le calcul d'une
forme normale de tête*.
Cela nécessite tout de même de «réduire sous les lambdas».
Ce faisant,
un terme d'un problème d'unification peut finir en forme -normale,
mais uniquement si la décision de l'unification l'exige.
On a donc une forme de -normalisation paresseuse.
Pour ce qui est de l'affichage des termes,
la normalisation des termes à afficher dépend des systèmes.
Dans le système 
*,
les termes ne sont pas -normalisés avant affichage,
mais il existe un prédicat prédéfini qui -normalise son argument.
C'est le seul endroit où le calcul d'une forme -normale est entrepris.
On voit donc que l'économie
de la -réduction n'est pas du tout
la même en programmation fonctionnelle et en Prolog.
Forme 
-normale.
n.f.
Terme du -calcul*
qui ne contient pas de -rédex*.
Forme normale conjonctive.
n.f.
(abr. 
)
Formule du calcul des prédicats qui est construite à l'aide
de quantifications universelles, de conjonctions,
de disjonctions, de négations et de
formules atomiques*,
de sorte que
aucune conjonction n'est dans la portée d'une disjonction,
aucune disjonction n'est dans la portée d'une négation,
et aucune quantification universelle n'est dans la portée d'une disjonction.
Ce sont donc des arbres tels que le chemin qui mène de la racine à chaque
feuille ait la forme suivante : 
.
La position précise des quantifications universelles parmi les conjonctions
importe peu.
On a tendance à les voir en position prénexe*
(
)
pour décrire la résolution*,
et sous toutes les conjonctions
(c'est-à-dire «entre» les conjonctions et les disjonctions,
)
pour décrire la structure des programmes Prolog*.
On peut toujours transformer une formule du calcul des prédicats classique
en une formule qui
est réfutable si et seulement si la formule originale l'est.
La sémantique n'est pas totalement conservée car la transformation introduit des
constantes nouvelles
( skolémisation*)
qui permettent de donner à la formule originale et
à la formule des interprétations différentes.
Forme normale -longue.
n.f.
Terme du -calcul* qui ne contient aucun
-rédex*
et où les variables et les constantes sont -expansées*
selon leurs types.
Forme normale pour la négation.
n.f.
Formule du calcul des prédicats où le connecteur de négation n'est
appliqué qu'à des
formule atomique*.
Par exemple,
est en forme normale pour la négation,
mais pas 
.
On peut toujours mettre une formule sous cette forme
en utilisant les lois de De Morgan.
Forme normale de tête.
n.f.
Terme du -calcul*
qui consiste en zéro ou plusieurs
-abstractions*
imbriquées dont le corps* de la
plus imbriquée n'est ni
un -rédex ni une application dont la
tête* est un -rédex.
Par exemple,
, 
,
sont des formes normales de tête, alors que
,
,
n'en sont pas.
Chacune de ces dernières se -réduit* en l'une des premières.
Le rédex 
n'empêche pas le troisième terme
d'être une forme normale de tête car seule la tête compte.
Forme normale de tête -longue.
n.f.
Forme normale de tête où la tête est
-expansée* selon son type.
C'est la forme préférée pour la manipulation des
-terme dans la procédure d´unification* modulo
-équivalence.
formule.
n.f.
ex.progr.
Constructeurs de formules logiques de niveau objet.
kind (formule, individu) type .
type (et, ou, impl) formule -> formule -> formule .
type non formule -> formule .
type (qqsoit, existe) (individu->formule) -> formule .
type (p, ...) individu -> individu -> formule .
type (q, ...) formule .
Tous ces constructeurs sauf qqsoit et existe peuvent aussi bien
être définis dans une variante typée de Prolog.
Les constructeurs qqsoit et existe sont typiques de Prolog.
Ils prennent comme unique argument une fonction de individu vers
formule.
Ces fonctions sont donc des prédicats du métalangage.
Formule atomique.
n.f.
Formule constituée d'un symbole prédicatif et de ses arguments,
et ne comportant pas de connecteur.
C'est la plus petite unité de sens propositionnel.