ACL2

Keywords: ACL2, Lisp, Wikipedia, NQTHM

ACL2 es un demostrador automatizado de teoremas con una lógica basada en un subconjunto aplicativo del lenguaje Common Lisp. También está escrito es ese mismo sublenguaje y puede correr en diversas implementaciones de Common Lisp. Tiene un alto grado de automatismo y los programas esccritos en ACL2 pueden ser ejecutados en Common Lisp directamente. ACL2 es la versión industrial del demostrador NQTHM de Boyer-Moore.

Enlaces externos

• http://www.cs.utexas.edu/users/moore/acl2/

Wikipedia. Puedes encontrar fuentes en las wikipedias en otras lenguas. Si lo amplias hasta el punto de que este cartel no sea necesario por favor, elimínalo.

Keywords: ACL2, Lisp, Wikipedia, NQTHM