miércoles, enero 25, 2006

ACL2 demostrador de teoremas


El día de hoy me llamó la atención ACL2 (Applicative Common LISP) el cual puede servir como un demostrador de teoremas. Por ahora me puse averiguar en que aplicaciones fue utilizado con exito, que vienen siendo los siguientes:

-Encontrar bugs en compiladores, al mismo tiempo que se valida el diseño.
-Probar sistemas complejos de hardware y software.





1 comentario:

Anónimo dijo...

Quizá te interese el
Otter
, que es más orientado a las matemáticas y no a la verificación de algoritmos como el acl2.