| dbo:abstract
|
- Στην επιστήμη υπολογιστών, το Coq είναι ένας (interactive theorem prover). Υποστηρίζει την έκφραση μαθηματικών βεβαιώσεων, ελέγχει μηχανικά αποδείξεις τους, βοηθά στην εύρεση τυπικών αποδείξεων και εξάγει ένα πιστοποιημένο πρόγραμμα (certified program) από μια κατασκευαστική απόδειξη των τυπικών προδιαγραφών του. Το Coq λειτουργεί στη θεωρία του λογισμού των επαγωγικών κατασκευών (calculus of inductive constructions), ο οποίος αποτελεί παράγωγο του λογισμού των κατασκευών (calculus of constructions). Το Coq δεν είναι αυτόματος αποδείκτης θεωρημάτων αλλά περιλαμβάνει και διάφορες διαδικασίες απόφασης (decision procedures). Το Coq υλοποιεί μια συναρτησιακή γλώσσα προγραμματισμού με εξαρτώμενους τύπους (dependent types). Αναπτύσσεται στη Γαλλία, στο εγχείρημα TypiCal (πρώην LogiCal), στο οποίο συμμετέχουν από κοινού το INRIA, η Πολυτεχνική Σχολή (École Polytechnique), το Πανεπιστήμιο Paris-Sud 11 και το . παλιότερα υπήρχε και μια ομάδα στην École Normale Supérieure de Lyon. Ο αρχηγός της ομάδας είναι ο Benjamin Werner. Το Coq υλοποιείται σε Objective Caml. Η λέξη coq σημαίνει "κόκορας" στα Γαλλικά και προκύπτει από μια παράδοση ονομασίας των Γαλλικών ερευνητικών εργαλείων με ονόματα ζώων. Αποτελεί επίσης αναφορά στον Τιερί Κοκάν (Thierry Coquand), ο οποίος ανέπτυξε το λογισμό των κατασκευών με το Ζεράρ Υ (Gérard Huet). Αρχικά, ονομαζόταν απλά Coc, τα αρχικά των λέξεων "calculus of construction". (el)
- Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving (procedures) and various decision procedures. The Association for Computing Machinery awarded Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, and Pierre Castéran with the 2013 ACM Software System Award for Coq. Coq is a wordplay on the name of Thierry Coquand, Calculus of Constructions or "CoC" and is following the French tradition to name tools after animals (coq in French meaning rooster). (en)
- Coq ist eine freie Software zum maschinengestützten Beweisen mathematischer Aussagen. (de)
- 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. Fue desarrollado en Francia, en el proyecto LogiCal, entre el INRIA, la École Polytechnique, la y el CNRS. Dirigen el desarrollo los investigadores Gilles Dowek y Christine Paulin-Mohring. Coq está escrito en el lenguaje . (es)
- Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 de l’Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon). Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand. Dans la même veine, son langage est Gallina et Coq possède un wiki dédié, baptisé Cocorico!. En 2013, Coq a été récompensé du Programming Languages Software Award par l'ACM SIGPLAN. Coq a reçu en 2022 le premier « prix science ouverte logiciel libre de la recherche » dans la catégorie « scientifique et technique ». (fr)
- Coqは、証明支援システムの一つ。Coqの核はプログラミング言語を用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。 (ja)
- Coq (фр. coq — півень) — інтерактивний програмний засіб доведення теорем, використовує власну мову функціонального програмування (Gallina) з залежними типами. Дозволяє записувати математичні теореми і їхні доведення, починаючи з цілі (гіпотези, яку потрібно довести). Coq може автоматично знаходити доведення в деяких обмежених теоріях за допомогою тактик. Coq використовується для верифікації програм. (uk)
- Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ. Coq разработан во Франции в рамках проекта TypiCal (ранее — LogiCal), совместно управляемом INRIA, Политехнической школой, Университетом Париж-юг XI и Национальным центром научных исследований, ранее была выделенная группа и в . Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана. (ru)
- Na ciência da computação, Coq é provador de teoremas interativo. Ele permite a expressão de asserções matemáticas, verifica mecanicamente as provas destas asserções, auxilia a encontrar provas formais e extrai um programa certificado a partir da prova construtiva de sua especificação formal. Coq trabalha dentro da teoria do cálculo de construções indutivas, derivada do cálculo de construções. Coq não é um provador de teoremas automatizado, mas inclui táticas automáticas de demonstração de teoremas e vários procedimentos de decisão. Coq é um software livre e de código aberto, licenciado sob a licença GNU Lesser General Public License Version 2.1. É escrito majoritariamente na linguagem de programação OCaml. A versão 8.8.2 foi lançada em 26 de setembro de 2018. Coq foi laureado com os prestigiosos prêmios ACM SIGPLAN Programming Languages Sofware Award, em 2013, e ACM Software System Award, em 2014. (pt)
- Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的（certified）程序。Coq 的理论基础是归纳构造演算（calculus of inductive constructions）、一种构造演算（calculus of constructions）的衍生理论。Coq 并非一个自动化定理机器证明语言；然而，它提供了自动化定理证明的策略（tactics）和不同的决策过程。 Coq 同时还是一个依赖类型的函数式编程语言。它由法国PPS实验室的PI.R2团队研究开发，该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法国国家科学研究中心组成。此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 、 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。 单词 coq 在法语中意为“公鸡”，此命名体现了法国在研究活动中使用动物名称命名工具的传统。 最初，它被简单地称作 Coc，意即构造演算（calculus of constructions）的缩写，同时也暗含了 Thierry Coquand（与 Gérard Huet 共同提出了前述的构造演算）的姓氏。 Coq 自身提供了一套规范语言 Gallina（gallina 在西班牙语中意为“母鸡”）。使用 Gallina 书写的程序具有规范化性质——它们总是会终止。此性质使之避开了停机问题。同时，这也使得 Coq 语言本身并非图灵完全。 (zh)
|
| rdfs:comment
|
- Coq ist eine freie Software zum maschinengestützten Beweisen mathematischer Aussagen. (de)
- Coqは、証明支援システムの一つ。Coqの核はプログラミング言語を用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。 (ja)
- Coq (фр. coq — півень) — інтерактивний програмний засіб доведення теорем, використовує власну мову функціонального програмування (Gallina) з залежними типами. Дозволяє записувати математичні теореми і їхні доведення, починаючи з цілі (гіпотези, яку потрібно довести). Coq може автоматично знаходити доведення в деяких обмежених теоріях за допомогою тактик. Coq використовується для верифікації програм. (uk)
- Στην επιστήμη υπολογιστών, το Coq είναι ένας (interactive theorem prover). Υποστηρίζει την έκφραση μαθηματικών βεβαιώσεων, ελέγχει μηχανικά αποδείξεις τους, βοηθά στην εύρεση τυπικών αποδείξεων και εξάγει ένα πιστοποιημένο πρόγραμμα (certified program) από μια κατασκευαστική απόδειξη των τυπικών προδιαγραφών του. Το Coq λειτουργεί στη θεωρία του λογισμού των επαγωγικών κατασκευών (calculus of inductive constructions), ο οποίος αποτελεί παράγωγο του λογισμού των κατασκευών (calculus of constructions). Το Coq δεν είναι αυτόματος αποδείκτης θεωρημάτων αλλά περιλαμβάνει και διάφορες διαδικασίες απόφασης (decision procedures). (el)
- Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving (procedures) and various decision procedures. (en)
- 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. (es)
- Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 de l’Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon). Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand. Dans la même veine, son langage est Gallina et Coq possède un wiki dédié, baptisé Cocorico!. (fr)
- Na ciência da computação, Coq é provador de teoremas interativo. Ele permite a expressão de asserções matemáticas, verifica mecanicamente as provas destas asserções, auxilia a encontrar provas formais e extrai um programa certificado a partir da prova construtiva de sua especificação formal. Coq trabalha dentro da teoria do cálculo de construções indutivas, derivada do cálculo de construções. Coq não é um provador de teoremas automatizado, mas inclui táticas automáticas de demonstração de teoremas e vários procedimentos de decisão. (pt)
- Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的（certified）程序。Coq 的理论基础是归纳构造演算（calculus of inductive constructions）、一种构造演算（calculus of constructions）的衍生理论。Coq 并非一个自动化定理机器证明语言；然而，它提供了自动化定理证明的策略（tactics）和不同的决策过程。 Coq 同时还是一个依赖类型的函数式编程语言。它由法国PPS实验室的PI.R2团队研究开发，该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法国国家科学研究中心组成。此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 、 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。 单词 coq 在法语中意为“公鸡”，此命名体现了法国在研究活动中使用动物名称命名工具的传统。 最初，它被简单地称作 Coc，意即构造演算（calculus of constructions）的缩写，同时也暗含了 Thierry Coquand（与 Gérard Huet 共同提出了前述的构造演算）的姓氏。 (zh)
- Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ. (ru)
|
