| German |
| has gloss | deu: Coq ist ein Programm zum maschinengestützten Beweisen mathematischer Aussagen. |
| lexicalization | deu: Coq |
| French |
| has gloss | fra: Coq est un assistant de preuve développé à lINRIA, à lÉcole polytechnique et à lUniversité de Paris XI (et antérieurement à lÉcole normale supérieure de Lyon) dans le cadre du projet TypiCal. |
| lexicalization | fra: Coq |
| Russian |
| has gloss | rus: В информатике, Coq есть доказатель теорем и язык функционального программирования с зависимыми типами. Он позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, (то есть гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ. |
| lexicalization | rus: Coq |
| Castilian |
| has gloss | spa: Coq (gallo en francés) 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. |
| lexicalization | spa: Coq |
