Abstract proof checking: An example motivated by an incompleteness theorem

DOI10.1023/A:1005877613942zbMath0890.03004OpenAlexW1558960796MaRDI QIDQ1373302

Toby Walsh, Alan Bundy, Adolfo Villafiorita, Fausto Giunchiglia

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)

Related Items (4)

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

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