Preuves compositionnelles en programmation logique.