Extraction de programmes à partir de spécifications en logique existentielle du second ordre par compilation de connaissances.