TY - JOUR
T1 - Abstract proof checking: an example motivated by an incompleteness theorem
AU - Bundy, Alan
AU - Giunchiglia, F.
AU - Villaļ¬orita, F.
AU - Walsh, T.
PY - 1997
Y1 - 1997
N2 - 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.
AB - 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.
KW - Abstraction
KW - proof checking
KW - incompleteness theorems
M3 - Article
VL - 19
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
SN - 0168-7433
IS - 3
ER -