Proof General: A Generic Tool for Proof Development
Proof General: A Generic Tool for Proof Development
复制标题
证明通用：证明开发的通用工具
DOI：
10.1007/3-540-46419-0_3
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
David Aspinall
中科院分区：
文献类型：
--
作者：
David Aspinall
本说明描述了证明通用，这是一种使用交互式证明助手开发机器证明的工具。互动是基于证明脚本的，这是证明开发的目标。 Proof General提供了一个强大的用户界面，努力相对较少，减轻了对助手提供自己的GUI的需求，并为多样化的证明助手提供了统一的优点。
Proof General的用户群不断增长，目前用于多种交互式证明系统，包括Coq，Lego和Isabelle。支持他人正在路上。在这里，我们简要概述了一般证明的作用及其背后的哲学。技术细节在其他地方可用。该程序和用户文档可在网络上找到，网址为http://www.dcs.ed.ac.uk/home/proofgen。
This note describes Proof General, a tool for developing machine proofs with an interactive proof assistant. Interaction is based around a proof script, which is the target of a proof development. Proof General provides a powerful user-interface with relatively little effort, alleviating the need for a proof assistant to provide its own GUI, and providing a uniformap pearance for diverse proof assistants.
Proof General has a growing user base and is currently used for several interactive proof systems, including Coq, LEGO, and Isabelle. Support for others is on the way. Here we give a brief overview of what Proof General does and the philosophy behind it; technical details are available elsewhere. The program and user documentation are available on the web at http://www.dcs.ed.ac.uk/home/proofgen.