Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
From MaRDI portal
Publication:3498463
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
Related Items
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
Cites Work
