Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #543 | |
|---|---|
| Title: | Automating Meta-Theory Creation and System Extension |
| Authors: | Basin,D; Giunchiglia,F; Traverso,P |
| Date: | 1991 |
| Presented: | Accepted at AI*IA (Italian Association for Artificial Intelligence), Palermo, Italy, 1991. Will appear in Springer LNAI Series. |
| Keywords: | |
| Abstract: | In this paper we describe a first experiment with a new approach for building theorem provers that can formalise themselves, reason about themselves, and safely extend themselves with new inference procedures. Within the GETFUL system we have built a pair of functions that operate between the system's implementation and a theory about this implementation. The first function lifts the actual inference rules to axioms that comprise a theory of GETFUL's inference capabilities. This allows us to turn the prover upon itself whereby we may formally reason about its inference rules and derive new rules. The second function flattens new rules back into the underlying system. This provides a novel means of safe system self-extension and an efficient way of executing derived rules. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}