ISSN:
1573-0670
Keywords:
abstraction
;
proof checking
;
incompleteness theorems
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract 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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1005877613942