Programmation logique contrainte
La programmation logique contrainte est une forme de programmation par contraintes, dans laquelle la programmation logique est étendue pour inclure les concepts de satisfaction de contraintes .
Un programme logique de contrainte est un programme logique qui contient par contre des entrainements dans le corps des clauses. Un exemple de clause incluant une contrainte est A (X, Y) : - X + Y > 0, B (X), C (Y) . Dans cette clause, X + Y > 0 est une contrainte; A (X, Y), B (X) et C (Y) sont des littéraux comme dans la programmation logique normale. Cet article indique une condition dans laquelle l'état A (X, Y) est vérifiée: X + Y est supérieur à zéro et bot h B (X) et C (Y) sont vraies.
Comme dans la programmation logique régulière, les programmes sont interrogés sur la prouvabilité d'un objectif, qui peut contenir des contraintes en plus des littéraux.
La preuve d'un objectif est composée de clauses dont les corps sont des contraintes satisfaisables et des littéraux qui peuvent à leur tour être prouvés à l'aide d'autres clauses. L'exécution est effectuée par un interprète, qui commence à partir de l'objectif et analyse de manière récursive les clauses essayant de prouver l'objectif. Les contraintes rencontrées lors de cette analyse sont placées dans un ensemble appelé magasin de contraintes . Si cet ensemble s'avère insatisfiable, l'interprète fait un retour en arrière en essayant d'utiliser d'autres clauses pour prouver l'objectif. En pratique, la satisfiabilité de la contrainte peut être vérifiée à l'aide d'un algorithme incomplet, qui ne détecte pas toujours les incohérences.
