Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs
复制标题
DOI：
10.1007/978-3-540-75560-9_13
复制
发表时间：
2007-10
期刊：
影响因子：
--
通讯作者：
Richard Bonichon;David Delahaye;Damien Doligez
中科院分区：
文献类型：
--
作者：
Richard Bonichon;David Delahaye;Damien Doligez
我们提出了Zenon，一个自动定理证明一阶经典逻辑（与平等），基于tableau方法。Zenon旨在成为Focal环境的专用证明器，Focal环境是一个面向对象的代数规范和证明系统，能够生成用于执行的OCaml代码和用于认证的Coq代码。Zenon可以直接生成Coq证明（证明脚本或证明术语），这些证明可以重新插入到由Focal生成的Coq规范中。Zenon也可以扩展，这使得Focal中的特定（可能是本地）自动化成为可能。
We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications produced by Focal. Zenon can also be extended, which makes specific (and possibly local) automation possible in Focal.