Unified Classical Logic Completeness
DOI10.1007/978-3-319-08587-6_4zbMATH Open1409.68250OpenAlexW128672336MaRDI QIDQ3192180FDOQ3192180
Authors: Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel 
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
Recommendations
- Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique
- Intuitionistic completeness and classical logic
- An intuitionistic completeness theorem for classical predicate logic
- A proof of the standard completeness for the involutive uninorm logic
- Uniform provability in classical logic
- Complete Coinductive Theories. I
- On the unification of classical, intuitionistic and affine logics
- On the completeness of propositional Hoare logic
- Provability logic and the completeness principle
- Monoidal logics: completeness and classical systems
Proof theory in general (including proof-theoretic semantics) (03F03) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Abstract data types; algebraic specification (68Q65)
Cited In (14)
- Formalization of the resolution calculus for first-order logic
- A formalized general theory of syntax with bindings
- Complete Coinductive Theories. I
- A formalized general theory of syntax with bindings: extended version
- Mechanised modal model theory
- Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- A formally verified abstract account of Gödel's incompleteness theorems
- Soundness and completeness proofs by coinductive methods
- Formalization of the Resolution Calculus for First-Order Logic
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Markov chains and Markov decision processes in Isabelle/HOL
- A naive prover for first-order logic: a minimal example of analytic completeness
- Title not available (Why is that?)
Uses Software
This page was built for publication: Unified Classical Logic Completeness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192180)
