Unified Classical Logic Completeness
From MaRDI portal
Publication:3192180
DOI10.1007/978-3-319-08587-6_4zbMath1409.68250OpenAlexW128672336MaRDI QIDQ3192180
Jasmin Christian Blanchette, Dmitriy Traytel, Andrei Popescu
Publication date: 26 September 2014
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-08587-6_4
Abstract data types; algebraic specification (68Q65) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)
Related Items
Soundness and completeness proofs by coinductive methods, Formalization of the resolution calculus for first-order logic, A formalized general theory of syntax with bindings, Markov chains and Markov decision processes in Isabelle/HOL, Unnamed Item, A formalized general theory of syntax with bindings: extended version, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality, A formally verified abstract account of Gödel's incompleteness theorems, Formalization of the Resolution Calculus for First-Order Logic, Mechanised modal model theory
Uses Software
