Automated proofs of Löb's theorem and Gödel's two incompleteness theorems

DOI10.1007/BF00244396zbMath0657.03007OpenAlexW2283907753MaRDI QIDQ1110495

Art Quaife

Publication date: 1988

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244396

zbMATH Keywords

modal logic K4automated reasoning system ITPprovability in formalized Peano arithmetic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items

Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version, Automated search for Gödel's proofs, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, A formally verified abstract account of Gödel's incompleteness theorems