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
|
Keywords: |
|
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.
|
Download: | POSTSCRIPT COPY
|