Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

DOI10.1007/978-3-540-75560-9_13zbMATH Open1137.68572OpenAlexW1878755246MaRDI QIDQ3498463FDOQ3498463

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

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

Mathematics Subject Classification ID

Cites Work

• The TPTP problem library. CNF release v1. 2. 1
• Title not available (Why is that?)
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Title not available (Why is that?)
• Autarkic computations in formal proofs
• Automated proof construction in type theory using resolution

Cited In (20)

• 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
• Functional Testing in the Focal Environment
• Automated proof of Bell-LaPadula security properties
• A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking
• Zenon
• Invariants for the FoCaL language
• Resolution is cut-free
• 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
• Integrating simplex with tableaux

Uses Software

• Coq
• TPTP
• Metis_
• Matita
• OCaml
• Gandalf
• Ivy

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)