Prolog est un langage de programmation abstrait qui appartient au paradigme de la programmation logique. Deux remarques s'imposent. Premièrement, nous qualifions Prolog de langage de programmation abstrait pour le distinguer des systèmes concrets qui sont mis à la disposition des utilisateurs. C'est ici que se voient des différences de schéma d'exécution comme la gestion de mémoire (voir la section «Langage et machine -- abstraite ou concrète»*). Deuxièmement, le paradigme de la programmation logique et le langage de programmation Prolog sont apparus simultanément, le second restant longtemps la seule instance du premier.
Le fondement logique de Prolog étant la théorie des clauses de Horn,
on a pu croire que la programmation logique était la programmation en clauses
de Horn et qu'elle laissait comme degré de liberté le domaine de calcul,
la stratégie de calcul,
ou la présence ou non de négation dans les questions ou les corps de clauses.
Jouer sur le domaine de calcul aboutit à la programmation logique avec
contrainte [Jaffar et Lassez 86, Van Hentenryck 89, Cohen 90, Colmerauer 90].
L'étude des stratégies aboutira à la définition de stratégies
«exotiques»
(car peu employées, comme le retour-arrière intelligent,
ou non-strictement descendantes,
comme la tabulation [Warren 92]),
ou à la possibilité de programmer la stratégie
(par exemple le freeze de Prolog 
[Colmerauer et al. 82])
ou d'en compiler une en se fondant sur une analyse du programme à
exécuter
(par exemple le système Mercury [Somogyi et al. 96]).
Des stratégies dédiées à l'exécution de Prolog sur des machines parallèles
ont aussi vu le jour [Chassin de Kergommeaux et Codognet 94].
Enfin,
la possibilité d'avoir des négations dans les buts et les questions Prolog
a inspiré une quantité énorme de
travaux [Clark 78, Apt et Bol 94].
Qu'ont donc ces clauses de Horn qui leur fait jouer un rôle si central ? En fait, elles satisfont l'objectif de la programmation logique qui est de considérer des formules comme des programmes et la construction de leurs preuves comme l'exécution de ces programmes. On peut résumer leurs propriétés en quatre points.
) indique
toujours quelle branche de la disjonction est vraie (
ou bien 
),
et que la preuve d'un énoncé existentiel (
) fournit toujours
la construction d'un 
tel que est vrai.
Il peut bien sûr y avoir plusieurs branches vraies ou plusieurs constructions
pour ;
elles pourront être énumérées.
Cette propriété fournit au paradigme de la programmation logique une notion de résultat : le résultat de l'exécution d'un programme (la recherche d'une preuve) est une représentation des valeurs qui rendent la question vraie.
Cela permet de faire le lien entre une sémantique logique et une sémantique procédurale [Kowalski 74, Kowalski et Van Emden 76]. Dans la première, le programme est considérée comme une conjonction de prédicats, alors que dans la seconde, il est considéré comme un ensemble de procédures. Malheureusement, on utilise le plus souvent une spécialisation de cette stratégie qui est incomplète.
Il faut noter que, comme souvent, la complétude calculatoire peut être obtenue avec une surprenante économie de moyen. En effet, le fragment des programmes de Horn limités à un prédicat formé d'une clause unitaire et d'une clause dont le corps est atomique est aussi calculatoirement complet [Devienne et al. 96].
Ce résultat permet de désigner un modèle particulier comme étant la sémantique dénotationnelle de Prolog. Malheureusement, c'est un résultat très «fragile» au sens où il résiste mal aux actions sur les degrés de libertés de la programmation logique en clause de Horn. Par exemple, les modèles choisis pour la programmation logique avec contrainte ne sont pas des modèles de Herbrand, et il n'a pas été facile de trouver une sémantique pour les clauses de Horn avec négation qui détermine un plus petit modèle, et en plus celui-ci est extrêmement difficile à calculer.
Une autre bonne propriété des formules de Horn est qu'elles
«ressemblent» à beaucoup d'autres formalismes basés sur des règles :
grammaires, réécriture, systèmes experts, déduction.
Même si ces formalismes ne sont pas équivalents,
la tâche de les mettre en 
uvre en programmation logique s'en trouve
simplifiée
(voir par exemple les sections
«
Prolog et grammaires formelles»* --
et «Des démonstrateurs enfouis»*).
Les formules de Horn ont donc de bonnes propriétés,
mais elles ne sont pas seules dans ce cas.
Par exemple,
la théorie des formules de Harrop
est aussi constructive dans le calcul des prédicats intuitionniste.
Une stratégie de recherche de preuve dite uniforme*
est complète pour ces formules
et peut aussi passer pour une sémantique opérationnelle.
La théorie de la programmation logique s'étant le plus souvent développée dans le cadre du calcul des prédicats classique, on peut s'inquiéter du changement de cadre de référence de classique vers intuitionniste. Il faut savoir que les théories de Horn ont les mêmes conclusions et les mêmes bonnes propriétés dans les deux cadres de références. Comme d'autre part les formules de Harrop sont une extension stricte des formules de Horn, le résultat de complétude calculatoire est aussi conservé.
Miller montre que des fragments d'autres logiques ont la propriété des preuves uniformes [Miller 94]. Il propose plus généralement que soit appelé langage de programmation logique abstrait tout fragment de logique qui a cette propriété [Miller et al. 91]. Le véritable glissement conceptuel n'est donc pas de passer de la logique classique à la logique intuitionniste, mais de passer d'un point de vue centré sur un aspect de la théorie de la démonstration (la résolution) à un point de vue centré sur la théorie des preuves en général. Il faut noter qu'on peut quand même retrouver une sorte de principe de résolution pour les formules de Harrop [Hui Bon Hoa 94, Hui Bon Hoa 97].