Bonjour, David Mentré a proposé la question suivante : Catégorie: Logiciels Question : De ACL2, Coq, HOL et PVS, lequel de ces logiciels n'est pas un assistant de preuve libre ? Réponse : PVS À modérer sur http://thomas.enix.org/trivialibre/moderation.php Bonne journée ! -- Trivialibre http://thomas.enix.org/trivialibre/