Foundational Proof Certificates in First-Order Logic
From MaRDI portal
Publication:4928436
DOI10.1007/978-3-642-38574-2_11zbMath1381.68261OpenAlexW107224311MaRDI QIDQ4928436
Zakaria Chihani, Fabien Renaud, Dale A. Miller
Publication date: 14 June 2013
Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-38574-2_11
Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
Proof checking and logic programming ⋮ Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations ⋮ The Proof Certifier Checkers ⋮ An Evaluation-Driven Decision Procedure for G3i ⋮ Proofs and Reconstructions ⋮ Unnamed Item ⋮ A semantic framework for proof evidence ⋮ Proof certificates for equality reasoning ⋮ Proof Checking and Logic Programming ⋮ Proof search and certificates for evidential transactions ⋮ A proof theory for model checking ⋮ Logic-independent proof search in logical frameworks (short paper)
Uses Software
