Sciweavers

LPAR
2007
Springer
14 years 6 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 ...
Richard Bonichon, David Delahaye, Damien Doligez