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.

References in zbMATH (referenced in 23 articles , 2 standard articles )

Showing results 1 to 20 of 23.
Sorted by year (citations)

1 2 next

  1. Cristiá, Maximiliano; Rossi, Gianfranco: Automated proof of Bell-LaPadula security properties (2021)
  2. Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
  3. Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui: EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract) (2019) arXiv
  4. Gilbert, Frédéric: Automated constructivization of proofs (2017)
  5. Cauderlier, Raphaël; Dubois, Catherine: ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti (2016)
  6. Dubois, Catherine; Pessaux, François: Termination proofs for recursive functions in FoCaLiZe (2016)
  7. Halmagrand, Pierre: Soundly proving B method formulæ using typed sequent calculus (2016)
  8. Bury, Guillaume; Delahaye, David: Integrating simplex with tableaux (2015)
  9. Dowek, Gilles: Deduction modulo theory (2015)
  10. Ronan Saillard: Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice (2015) not zbMATH
  11. Delahaye, David; Doligez, Damien; Gilbert, Frédéric; Halmagrand, Pierre; Hermant, Olivier: Zenon modulo: when Achilles outruns the tortoise using deduction modulo (2013)
  12. Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine: Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover (2012)
  13. Merz, Stephan; Vanzetto, Hernán: Automatic verification of TLA(^ + ) proof obligations with SMT solvers (2012)
  14. Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine: Verifying B proof rules using deep embedding and automated theorem proving (2011)
  15. Chaudhuri, Kaustuv; Doligez, Damien; Lamport, Leslie; Merz, Stephan: Verifying safety properties with the TLA(^ + ) proof system (2010) ioport
  16. Hermant, Olivier: Resolution is cut-free (2010)
  17. Lescuyer, Stéphane; Conchon, Sylvain: Improving Coq propositional reasoning using a lazy CNF conversion scheme (2009)
  18. Rioboo, Renaud: Invariants for the FoCaL language (2009)
  19. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
  20. Bezem, Marc; Hendriks, Dimitri: On the mechanization of the proof of Hessenberg’s theorem in coherent logic (2008)

1 2 next