Edinburgh Research Explorer

Abstract proof checking: an example motivated by an incompleteness theorem

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Original languageEnglish
Journalthe Journal of Automated Reasoning
Issue number3
Publication statusPublished - 1997


We demonstrate the use of abstraction in aiding the construction of aninteresting and difficult example in a proof-checking system. Thisexperiment demonstrates that abstraction can make proofs easier tocomprehend and to verify mechanically. To support such proof checking, wehave developed a formal theory of abstraction and added facilities for usingabstraction to the GETFOL proof-checking system.

    Research areas

  • Abstraction, proof checking, incompleteness theorems

ID: 402512