摘要：通过这些笔记，我们可以快速了解Coq系统，并展示它如何用于定义逻辑概念和函数，并对其进行推理。这是一个教程，读者可以快速开始自己的实验，只学习系统的一部分功能。[1]提供了更全面的研究，并提供了大量的练习来训练。
作者：Yves Bertot (INRIA Sophia Antipolis)
论文ID：cs/0603118
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-11-07
PDF 下载： 英文版 中文版pdf翻译中