The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #809

Title:An Incompleteness Theorem Via Abstraction
Authors:Bundy,A; Giunchiglia,F; Villafiorti,A; Walsh,T
Date:May 1996
Presented:Submitted to J A R
Abstract:We deomonstrate the use of abstraction in aiding the construction of an interesting and difficult example in a proof checking system. This experiment demonstrates that abstraction can make proofs easier to comprehend and to verify mechanically. To support such proof checking, we have developed a formal theory of abstraction and added facilities for using abstraction to the GETFOL proof checking system.

[Search These Pages] [DAI Home Page] [Comment]