Sciweavers

Share
LPAR
2007
Springer

Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs

10 years 5 months ago
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs
Abstract. 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 objectoriented 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.
Richard Bonichon, David Delahaye, Damien Doligez
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where LPAR
Authors Richard Bonichon, David Delahaye, Damien Doligez
Comments (0)
books