Zenon swMATH ID: 6753 Software Authors: Bonichon, Richard; Delahaye, David; Doligez, Damien Description: Zenon: An extensible automated theorem prover producing checkable proofs. 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. Homepage: http://deducteam.gforge.inria.fr/zenonmodulo/ Related Software: Coq; TPTP; dedukti; Isabelle/HOL; FoCaLiZe; BWare; z3; PVS; iProver; E Theorem Prover; Atelier B; Twelf; ArchSAT; CoqInE; SIMPLIFY; Why3; OCaml; SMT-LIB; Isabelle; Ivy Cited in: 20 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Zenon modulo: when Achilles outruns the tortoise using deduction modulo. Zbl 1406.68105Delahaye, David; Doligez, Damien; Gilbert, Frédéric; Halmagrand, Pierre; Hermant, Olivier 2013 Zenon: An extensible automated theorem prover producing checkable proofs. Zbl 1137.68572Bonichon, Richard; Delahaye, David; Doligez, Damien 2007 all top 5 Cited by 29 Authors 6 Delahaye, David 5 Dubois, Catherine 3 Halmagrand, Pierre 3 Hermant, Olivier 2 Berkani, Karim 2 Bury, Guillaume 2 Cauderlier, Raphaël 2 Doligez, Damien 2 Gilbert, Frédéric 2 Jacquel, Mélanie 1 Bezem, Marc 1 Bonichon, Richard 1 Burel, Guillaume 1 Carlier, Matthieu 1 Conchon, Sylvain 1 Cristiá, Maximiliano 1 Dowek, Gilles 1 Gallicchio, James 1 Hendriks, Dimitri 1 Lescuyer, Stéphane 1 Merz, Stephan 1 Mitsch, Stefan 1 Pessaux, François 1 Platzer, André 1 Rioboo, Renaud 1 Rossi, Gianfranco 1 Sutcliffe, Geoff 1 Tan, Yong Kiam 1 Vanzetto, Hernán Cited in 2 Serials 5 Journal of Automated Reasoning 1 Annals of Mathematics and Artificial Intelligence Cited in 3 Fields 18 Computer science (68-XX) 9 Mathematical logic and foundations (03-XX) 1 General algebraic systems (08-XX) Citations by Year