ACL2
De Wikipedia, la enciclopedia libre
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 escritos en ACL2 pueden ser ejecutados en Common Lisp directamente. ACL2 es la versión industrial del demostrador NQTHM de Boyer-Moore.
El lenguaje de programación ACL2 es una variante aplicativa de Common LISP. ACL2 es un lenguaje sin tipos debido a que todas las funciones de ACL2 son totales –es decir, toda función asocia a cada valor de espacio de valores de ACL2 otro valor de ese espacio.
La teoría de base de ACL2 axiomatiza la semántica de los lenguajes de programación y de sus funciones predefinidas. Cuando las definiciones del usuario satisfacen un principio de definición extienden la teoría de forma de mantener la consistencia lógica de la teoría.
La base del motor de demostración de ACL2 está basada en reescritura de términos, y se extiende con la inclusión de teoremas demostrados en el sistema que pueden ser utilizados como técnicas de prueba específicas en las conjeturas por demostrar.
El objetivo de los creadores de ACL2 fue realizar una versión del demostrador NQTHM de Boyer-Moore que pudiera ser utilizado en medio industrial. En base a ese objetivo, ACL2 contiene muchas características que apoyan el desarrollo limpio de teorías matemáticas y computacionales interesantes. ACL2 obtiene eficiencia gracias a que está escrito en Common LISP; Por ejemplo, la misma especificación que es la base para una verificación inductiva puede ser compilada y ejecutada en código nativo.
El nombre ACL2' viene de la abreviación ACL, que se extiende como A Computational Logic y como Applicative Common LISP.
