| dbo:abstract
|
- ACL2 ("A Computational Logic for Applicative Common Lisp") is a software system consisting of a programming language, created by Timothy Still it was an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for the purpose of software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software. (en)
- ACL2 es, a la vez, un lenguaje de programación, una lógica matemática para especificar y demostrar formalmente propiedades de los programas escritos en dicho lenguaje, y un que asiste al usuario en dicha tarea. ACL2 es la versión industrial del demostrador de R. Boyer y J S. Moore. En la actualidad está desarrollado por J S. Moore y M. Kaufmann en la Universidad de Texas en Austin. El nombre ACL2 es una abreviatura de A Computational Logic for an Applicative Common LISP. El lenguaje de programación ACL2 es un subconjunto de . 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 del universo de ACL2 otro valor de ese universo. Los programas escritos en ACL2 pueden ser ejecutados en Common Lisp directamente. El propio ACL2 está desarrollado usando su mismo lenguaje aplicativo. Una característica importante de ACL2 es que se usa el mismo lenguaje tanto para la implementación de los programas como para la especificación de sus propiedades. La lógica de ACL2 es un subconjunto de la lógica de primer orden. Sus fórmulas no tienen cuantificadores y las variables de una fórmula se consideran (implícitamente) universalmente cuantificadas. La teoría de base de ACL2 axiomatiza la semántica de su lenguaje de programación y de sus funciones predefinidas, tal y como se describen en el estándar Common Lisp. Cuando las definiciones del usuario satisfacen un cierto principio de definición extienden la teoría con el correspondiente axioma de definición. Grosso modo, el principio de definición garantiza que la función definida termina para todas las entradas posibles, manteniendo así la consistencia lógica de la teoría. El demostrador de ACL2 puede considerarse como un asistente para la demostración de teoremas en la lógica de ACL2. El motor de demostración de ACL2 está basado principalmente en la y en la automatización del principio de inducción. Aunque en principio ACL2 puede ser considerado un demostrador automático (una vez introducida una conjetura, procede de manera automática en su intento de demostración), el sistema es interactivo en un sentido más profundo. El papel del usuario en una formalización típica con ACL2 consiste en: a) definir las funciones que implementan el sistema que se quiere verificar, b) escribir la especificación del mismo, expresando las propiedades formales que se desean verificar y c) guiar al demostrador hacia una demostración automática de dicha especificación. La manera principal mediante la cual el usuario guía al demostrador consiste en la demostración de lemas previos que se incluyen en el sistema como reglas de y que son usados en la demostración de posteriores resultados. Los lemas específicos necesarios para cada demostración pueden venir sugeridos de una demostración (manual) preconcebida o bien, a más bajo nivel, de la inspección de la salida generada por un intento de demostración automática fallido. El objetivo de los creadores de ACL2 fue realizar una versión del demostrador de Boyer-Moore que pudiera ser utilizado para aplicaciones de escala industrial. Por ese objetivo, ACL2 contiene muchas características que permiten el desarrollo limpio de teorías matemáticas y computacionales. Además, ACL2 obtiene eficiencia gracias a que está escrito en Common LISP. Así, la misma especificación que es la base para una verificación formal puede ser compilada y ejecutada en código nativo. La principal aplicación de ACL2 se encuentra en la verificación formal de sistemas hardware cuya seguridad es crítica. Dichos sistemas son modelados en el lenguaje de programación y las propiedades que aseguran su corrección son formalmente verificadas. El hecho de que el modelo pueda ser ejecutado de manera eficiente permite además que pueda ser usado como un simulador del sistema modelado. En el año 2005, la ACM concedió el premio de software al demostrador de teoremas de Boyer y Moore (lo que incluye tanto a como a ACL2). Literalmente, el premio se concede a R. Boyer, M. Kaufmann y J S. Moore por ser precursores y autores "del más efectivo demostrador de teoremas como una herramienta de métodos formales para la verificación de hardware y software cuya seguridad es crítica". (es)
- ACL2（A Computational Logic for Applicative Common Lisp，应用式 Common Lisp 计算逻辑）是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2 从设计上支持基于归纳逻辑理论的自动推理，可应用于软件或硬件系统的形式化验证。ACL2 的编程语言及其实现基于 Common Lisp。ACL2 是基于BSD授权发布的开源软件。 (zh)
|
| dbo:designer
| |
| dbo:developer
| |
| dbo:influencedBy
| |
| dbo:latestReleaseVersion
| |
| dbo:license
| |
| dbo:thumbnail
| |
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 5365 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:bodystyle
| |
| dbp:designer
|
- Robert S. Boyer, J Strother Moore and Matt Kaufmann (en)
|
| dbp:developer
|
- Matt Kaufmann and J Strother Moore (en)
|
| dbp:influencedBy
| |
| dbp:latestReleaseVersion
| |
| dbp:license
| |
| dbp:logo
|
- ACL2 Logo 2014 transparent.png (en)
|
| dbp:name
| |
| dbp:operatingSystem
| |
| dbp:paradigm
| |
| dbp:typing
| |
| dbp:website
| |
| dbp:wikiPageUsesTemplate
| |
| dbp:year
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| rdfs:comment
|
- ACL2 ("A Computational Logic for Applicative Common Lisp") is a software system consisting of a programming language, created by Timothy Still it was an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for the purpose of software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software. (en)
- ACL2（A Computational Logic for Applicative Common Lisp，应用式 Common Lisp 计算逻辑）是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2 从设计上支持基于归纳逻辑理论的自动推理，可应用于软件或硬件系统的形式化验证。ACL2 的编程语言及其实现基于 Common Lisp。ACL2 是基于BSD授权发布的开源软件。 (zh)
- ACL2 es, a la vez, un lenguaje de programación, una lógica matemática para especificar y demostrar formalmente propiedades de los programas escritos en dicho lenguaje, y un que asiste al usuario en dicha tarea. ACL2 es la versión industrial del demostrador de R. Boyer y J S. Moore. En la actualidad está desarrollado por J S. Moore y M. Kaufmann en la Universidad de Texas en Austin. El nombre ACL2 es una abreviatura de A Computational Logic for an Applicative Common LISP. (es)
|
| rdfs:label
|
- ACL2 (en)
- ACL2 (es)
- ACL2 (zh)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:depiction
| |
| foaf:homepage
| |
| foaf:isPrimaryTopicOf
| |
| foaf:name
| |
| foaf:page
| |
| is dbo:knownFor
of | |
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is dbp:knownFor
of | |
| is foaf:primaryTopic
of | |