Unified Classical Logic Completeness

DOI10.1007/978-3-319-08587-6_4MaRDI QIDQ3192180zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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)

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

Cited in

(15)

• 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
• Formalized proof systems for propositional logic
• 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
• Completeness theorems for first-order logic analysed in constructive type theory
• Soundness and completeness proofs by coinductive methods
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formalization of the Resolution Calculus for First-Order Logic
• Markov chains and Markov decision processes in Isabelle/HOL
• A naive prover for first-order logic: a minimal example of analytic completeness

Describes a project that uses

Uses Software

• Archive Formal Proofs
• FOL Fitting
• Abstract Completeness
• Completeness theorem
• HOL
• Isabelle/HOL

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)