Abstract proof checking: An example motivated by an incompleteness theorem

DOI10.1023/A:1005877613942MaRDI QIDQ1373302zbMATH OpenOpenAlexFDO

Authors Alan Bundy, Fausto Giunchiglia, Adolfo Villafiorita, Toby Walsh

Publication date 29 June 1998

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

Full work available at URL https://doi.org/10.1023/a:1005877613942

zbMATH Keywords

abstractionproof checkinginteractive proof checker GETFOL

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4164177
• An automatic proof of Gödel's incompleteness theorem
• scientific article; zbMATH DE number 4009856
• scientific article; zbMATH DE number 2185701
• scientific article; zbMATH DE number 3880145

Cited in

(6)

• A New and Formalized Proof of Abstract Completion
• Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
• A formally verified abstract account of Gödel's incompleteness theorems
• Automated search for Gödel's proofs
• scientific article; zbMATH DE number 1759674 (Why is no real title available?)
• Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version

This page was built for publication: Abstract proof checking: An example motivated by an incompleteness theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1373302)