L'idée principale n'est pas de faire du Prolog mais d'intégrer dans Axiom un système de vérification formel pour prouver des parties de l'Algèbre. Une très très vaste tache. Un candidat est ACL2 (il repose sur le même Gnu Common Lisp qu'Axiom) : http://www.cs.utexas.edu/users/moore/acl2/(...)
[^] # A propos de "integrate logic programming"
Posté par David Mentré (site web personnel) . En réponse à la dépêche Axiom outragé, Axiom martyrisé mais Axiom libéré !. Évalué à 2.
Amicalement,
d.