( norm_nég (F i) (G i) ) . ( norm_nég (F i) (G i) ) . ( norm_nég (non (F i)) (G i) ) . ( norm_nég (non (F i)) (G i) ) .
Négation.
n.f.
(
formules héréditaires de Harrop*)
Le langage des formules de 
Prolog est une présentation dissymétrique
(voir la section
«Les formules héréditaires de Harrop»*)
du langage où les connecteurs «et» et «implique» (
et 
),
et le quantificateur «quel que soit» (
),
sont utilisés sans restriction et interprétés intuitionnistiquement.
On peut se demander si il est possible d'introduire une forme de négation
comme cela a été longuement étudié pour Prolog [Apt et Bol 94].
On peut bien sûr adopter l'implémentation cavalière de la négation par l'échec qui est aussi souvent adoptée en Prolog. Il s'agit d'utiliser le prédicat suivant :
type not o -> o .
not P :- P , ! , fail .
not P .
La sémantique de la négation par l'échec en relation avec la logique intuitionniste n'a été que très peu étudiée [Bonner et McCarty 90, Giordano et Olivetti 92]. Il n'y a pour l'instant aucun résultat aussi profond qu'en Prolog.
Une autre voie est de considérer la négation minimale [Momigliano 92]. Cette forme de négation a l'avantage d'être définissable dans le langage des formules de Harrop.
type neg o -> o .
neg P :- P => fail .
Il faut noter que la formule niée apparaît en position de prémisse d'une implication. Elle doit donc être de la nature d'une clause : par exemple, ne pas être une disjonction ou ne pas contenir certaines occurrences de quantifications existentielles.
La prouvabilité uniforme n'est pas complète pour la logique minimale, mais on peut, par une technique proche de celle de la double négation, transformer toute formule de Harrop avec négation en une formule qui est prouvable uniformément si et seulement si elle est un théorème de la logique minimale.
Négatif.
adj.
(ant. positif*)
1)
( polarité*)
2) Se dit d'un littéral* constitué d'une formule atomique* niée.
Normalisation forte.
n.f.
Propriété d'un système de réécriture selon laquelle toute
dérivation converge vers une forme normale.
Le -calcul* n'a pas cette propriété.
En effet,
des -termes n'ont pas de forme normale :
par exemple 
*,
car 
et c'est la seule réduction possible.
D'autres en ont une,
mais sont aussi le point de départ de dérivations qui ne convergent pas :
par exemple (
* 
* ),
car 
en 
-réduisant* le rédex
en premier,
mais
en -réduisant le rédex de à chaque fois.
En revanche,
le -calcul simplement typé*
et tous ceux du cube de Barendregt*
sont fortement normalisables.