Demostradores de teoremas Demostradores de teoremas 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. ...Wikipedia "ACL2"
El Cálculo de Construcciones (CoC) es un lambda-cálculo tipificado de alto nivel que contiene un álgebra de tipos. CoC permite definir funciones por ejemplo, de enteros en tipos, de tipos en tipos al igual que las fuciones de enteros en enteros. El cálculo de contrucciones tiene la propiedad de normalización fuerte. El desarrollador inicial de CoC fue Thierry Coquand en el INRIA, Francia. ...Wikipedia "Cálculo de Construcciones"
Coq ( gallo en francés) es un sistema de ayuda a la demostración de teoremas que maneja aserciones matemáticas, verifica mecánicamente las pruebas de aserciones, ayuda a encontrar pruebas para esas aserciones y extrae programas certificados (correctos) a partir de las pruebas constructivas de aserciones que representan su especificación formal. Coq trabaja en base a la teoría del Cálculo de Construcciones Inductivas, que es una teoría derivada del Cálculo de Construcciones. ...Wikipedia "Coq"
El demostrador interactivo de teoremas Isabelle es una herramienta, de ayuda a la demostración de teoremas escrita en el lenguaje de programación ML y desarrollada por Larry Paulson de la Universidad de Cambridge y Tobias Nipkow del Technische Universität München. ...Wikipedia "Demostrador de teoremas Isabelle"
LCF es un demostrador de teoremas interactivo desarrollado en la Universidad de Edimburgo y la Universidad de Stanford por Robin Milner y otros. ...Wikipedia "LCF"
This article is licensed under the GNU Free Documentation License.
It uses material from the Wikipedia . Direct links to the original articles are in the text.
If you use exact copy or modified of this article you should preserve above paragraph and put also : It uses material from
the Shortopedia article about "Demostradores de teoremas".
| MAIN PAGE | MAIN INDEX | CONTACT US |