Foundational Proof Certificates in First-Order Logic
From MaRDI portal
Publication:4928436
DOI10.1007/978-3-642-38574-2_11zbMath1381.68261MaRDI 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
03B10: Classical first-order logic
03B35: Mechanization of proofs and logical operations
03B20: Subsystems of classical logic (including intuitionistic logic)
Related Items
Unnamed Item, Proof Checking and Logic Programming, A semantic framework for proof evidence, Proof certificates for equality reasoning, Proof search and certificates for evidential transactions, Logic-independent proof search in logical frameworks (short paper), A proof theory for model checking, Proof checking and logic programming, An Evaluation-Driven Decision Procedure for G3i, Proofs and Reconstructions, Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations, The Proof Certifier Checkers
Uses Software