Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

DOI10.1007/978-3-540-75560-9_13zbMath1137.68572OpenAlexW1878755246MaRDI QIDQ3498463

Damien Doligez, David Delahaye, Richard Bonichon

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

Related Items (16)

Integrating Simplex with Tableaux ⋮ Invariants for the FoCaL language ⋮ Soundly Proving B Method Formulæ Using Typed Sequent Calculus ⋮ ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Automated Constructivization of Proofs ⋮ On the mechanization of the proof of Hessenberg's theorem in coherent logic ⋮ Resolution is cut-free ⋮ Automated proof of Bell-LaPadula security properties ⋮ Functional Testing in the Focal Environment ⋮ Zenon ⋮ Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving ⋮ Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme ⋮ Theorem proving as constraint solving with coherent logic ⋮ Implicit definitions with differential equations for KeYmaera X (system description)

Uses Software

• Unnamed Item
• TPTP
• Metis_
• Matita
• OCaml
• Gandalf
• Ivy

Cites Work

• Unnamed Item
• Unnamed Item
• The TPTP problem library. CNF release v1. 2. 1
• Autarkic computations in formal proofs
• Automated proof construction in type theory using resolution
• Source-Level Proof Reconstruction for Interactive Theorem Proving

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