Une sémantique opérationelle instrumentale pour Prolog et son application à la preuve de consistance d'un modèle d'interprétation abstraite.