Un paradigme de programmation et de raisonnement où les programmes sont exprimés par des ensembles de clauses logiques et où l'exécution procède par recherche dirigée de preuves, utilisant typiquement unification et retour arrière pour trouver des dérivations satisfaisant des buts.

Principe

Écrire des spécifications sous forme de faits et de règles ; interpréter le calcul comme la tentative de prouver un but à partir de ces règles via résolution ou SLD-résolution, l'unification instanciant les variables et le retour arrière explorant les alternatives.

Démonstration

Programme de type Prolog pour un arbre généalogique : des faits décrivent la relation parent et des règles définissent l'ancêtre comme la clôture transitive ; la requête ancestor(X,Y) déclenche une recherche qui unifie des variables et recule pour énumérer les solutions.

Mauvaise application

Traiter un programme logique comme du code impératif pur et s'appuyer sur des prédicats à effets de bord ou des constructions dépendantes de l'ordre compromet la sémantique déclarative et rend le raisonnement sur la correction difficile.

Conséquence

Une utilisation correcte produit des programmes concis et déclaratifs, un contrôle de recherche inhérent via le retour arrière, et de fortes capacités de méta-programmation et de raisonnement symbolique ; facilite aussi le prototypage rapide d'applications de recherche.

Inversion

Basculer vers la programmation fonctionnelle ou impérative où le calcul est donné par l'évaluation déterministe de fonctions ou par des commandes ordonnées au lieu de la recherche de preuves ; cela met l'accent sur le flux de contrôle plutôt que sur la spécification logique.

Limite

Concerne typiquement des fragments de clauses de Horn et une sémantique opérationnelle dirigée par des buts ; exclut les théories du premier ordre arbitraires au comportement de résolution non interprété, et la terminaison et la complétude ne sont pas garanties sans restrictions.

Tension sémantique

Tension entre lectures modèle-théorique (déclarative) et opérationnelle (procédurale) : le même programme peut être vu comme une spécification de conséquences logiques ou comme une recette opérationnelle dont le comportement dépend de la stratégie d'évaluation.

Synthèse

La programmation logique considère les programmes comme des théories logiques et la computation comme preuve automatisée : en encodant le savoir en clauses, on utilise unification et retour arrière pour réaliser des spécifications déclaratives via une recherche dirigée par des buts.