Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

DOI10.1007/978-3-540-75560-9_13MaRDI QIDQ3498463zbMATH OpenOpenAlexFDO

Authors Richard Bonichon, David Delahaye, Damien Doligez

Publication date 15 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00315920/file/bonichon-delahaye-doligez-lpar-2007.pdf

Mathematics Subject Classification ID

Recommendations

• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover
• Zeno: an automated prover for properties of recursive data structures
• An automated prover for Zermelo-Fraenkel set theory in Theorema
• Some applications of Gentzen's proof theory in automated deduction

Cites work

• scientific article; zbMATH DE number 1614710 (Why is no real title available?)
• scientific article; zbMATH DE number 3300566 (Why is no real title available?)
• Autarkic computations in formal proofs
• Automated proof construction in type theory using resolution
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• The TPTP problem library. CNF release v1. 2. 1

Cited in

(20)

• Integrating simplex with tableaux
• Implicit definitions with differential equations for KeYmaera X (system description)
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Automated constructivization of proofs
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Automated proof of Bell-LaPadula security properties
• Functional Testing in the Focal Environment
• A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking
• Zenon
• Resolution is cut-free
• Invariants for the FoCaL language
• An automated prover for Zermelo-Fraenkel set theory in Theorema
• Theorem proving as constraint solving with coherent logic
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover
• Zeno: an automated prover for properties of recursive data structures
• Soundly proving B method formulæ using typed sequent calculus
• ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
• Verifying B proof rules using deep embedding and automated theorem proving

Describes a project that uses

Uses Software

• Ivy
• Gandalf
• OCaml
• Matita
• Metis
• TPTP
• Coq

This page was built for publication: Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3498463)