Formalization and Reasoning in a Reflective Architecture

Presented at the IJCAI Workshop "Reflection and Metalevel Architectures and their Applications in AI", IJCAI'95, Montreal, Canada, July 1995.

---

Authors

Harald Rueß, Holger Pfeifer, and F.W. von Henke

Abstract

This paper is concerned with developing a reflective architecture for formalizing and reasoning about entities that occur in the process of software development, such as specifications, theorems, programs, and proofs. The starting point is a syntactic extension of the type theory ECC. An encoding of this object calculus within itself comprises the meta-level, and reflection principles are provided for switching between different levels. These reflection principles are used to mix object- and meta-level reasoning, to generate ``standard'' units by executing meta-operators, and to apply formal tactics that allow for abstraction from the basic inference rules.

gzipped postscript or postscript

BibTeX Entry

@inproceedings{,
	TITLE = {Formalization and Reasoning in a Reflective Architecture},
	AUTHOR = {Harald Rue{\ss} and Holger Pfeifer and F.W. von Henke},
	BOOKTITLE = {Reflection and Metalevel Architectures and their Applications in AI},
	EDITOR = {M.H. Ibrahim},
	NOTE = {IJCAI'95 Workshop},
	MONTH = jul,
	YEAR = 1995,
	ADDRESS = {Montreal, Canada}
}

---

Harald Ruess: ruess@csl.sri.com