Abstract proof checking: An example motivated by an incompleteness theorem

DOI10.1023/A:1005877613942zbMATH Open0890.03004OpenAlexW1558960796MaRDI QIDQ1373302FDOQ1373302

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

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

zbMATH Keywords

abstractionproof checkinginteractive proof checker GETFOL

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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
• Title not available (Why is that?)
• 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)