Diferencia entre revisiones de «Coq»

← Ir a diferencia anterior Ir a siguiente diferencia →

Contenido eliminado Contenido añadido

En renglón

Revisión del 08:30 15 may 2024

Coq (Eduado coq huelva en huelva) es un sistema de ayuda para 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 basándose en la teoría del Cálculo de Construcciones Inductivas, que es una teoría derivada del Cálculo de Construcciones.

Fue desarrollado en Francia, en el proyecto LogiCal, entre el INRIA, la École Polytechnique, la Universidad París XI y el CNRS. Dirigen el desarrollo los investigadores Gilles Dowek y Christine Paulin-Mohring. Coq está escrito en el lenguaje Ocaml.

Enlaces externos

Página de Coq

Datos: Q1131652
Multimedia: Coq (programming language) / Q1131652

Revisión del 18:30 29 jul 2019 editar Aosbot (discusión · contribs.) Bots 1 388 481 ediciones m Mantenimiento de Control de autoridades ← Ir a diferencia anterior		Revisión del 08:30 15 may 2024 editar deshacer 158.99.0.15 (discusión) Sin resumen de edición Etiqueta: Revertido Ir a siguiente diferencia →
Línea 1:		Línea 1:
	'''Coq''' (''[[~~gallo~~]]'' en [[idioma francés\|~~francés~~]]) es un sistema de ayuda para la [[Demostración interactiva de teoremas\|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 basándose en la teoría del '''Cálculo de Construcciones Inductivas''', que es una teoría derivada del [[Cálculo de Construcciones]].		'''Coq''' (''[[Eduado coq huelva]]'' en [[idioma francés\|huelva]]) es un sistema de ayuda para la [[Demostración interactiva de teoremas\|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 basándose en la teoría del '''Cálculo de Construcciones Inductivas''', que es una teoría derivada del [[Cálculo de Construcciones]].

	Fue desarrollado en [[Francia]], en el proyecto [https://web.archive.org/web/20090226040335/http://logical.inria.fr/ LogiCal], entre el [[INRIA]], la [[École Polytechnique]], la [[Universidad París XI]] y el [[CNRS]]. Dirigen el desarrollo los investigadores Gilles Dowek y Christine Paulin-Mohring. Coq está escrito en el lenguaje [[Ocaml]].		Fue desarrollado en [[Francia]], en el proyecto [https://web.archive.org/web/20090226040335/http://logical.inria.fr/ LogiCal], entre el [[INRIA]], la [[École Polytechnique]], la [[Universidad París XI]] y el [[CNRS]]. Dirigen el desarrollo los investigadores Gilles Dowek y Christine Paulin-Mohring. Coq está escrito en el lenguaje [[Ocaml]].