Mechanizing Mathematical Reasoning
From MaRDI portal
Publication:5717439
DOI10.1007/b106663zbMath1098.03026OpenAlexW2484955858MaRDI QIDQ5717439
Wilfried Sieg, Saverio Cittadini
Publication date: 10 January 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b106663
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items (11)
Proofs as Objects ⋮ Proof-Search in Natural Deduction Calculus for Classical Propositional Logic ⋮ Proofs, Upside Down ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ The polarized \(\lambda\)-calculus ⋮ A User-friendly Interface for a Lightweight Verification System ⋮ Automated search for Gödel's proofs ⋮ The Cantor–Bernstein theorem: how many proofs? ⋮ Human-centered automated proof search ⋮ NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
This page was built for publication: Mechanizing Mathematical Reasoning