English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Automating Meta-Theory Creation and System Extension

MPS-Authors
There are no MPG-Authors in the publication available
External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Basin, D., Giunchiglia, F., & Traverso, P. (1991). Automating Meta-Theory Creation and System Extension. In E. Ardizzone, S. Gaglio, & F. Sorbello (Eds.), Trends in Artificial Intelligence (pp. 48-57). Berlin: Springer.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0023-CF13-D
Abstract
In this paper we describe a first experiment with a new approach for building theorem provers that can formalize themselves, reason about themselves, and safely extend themselves with new inference procedures. Within the \tt GETFOL} system we have built a pair of functions that operate between the system's implementation and a theory about this implementation. The first function {\em lifts\/} the actual inference rules to axioms that comprise a theory of {\tt GETFOL}'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 {\em 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.