Axiomatizing Reflective Logics and Languages

Jose Meseguer and Manuel G. Clavel (SRI International)

PostScript

Adobe PDF

The very success and breadth of reflective techniques underscores the need for a general theory of reflection. At present what we have is a wide-ranging variety of reflective systems, each explained in its own idiosyncratic terms. Metalogical foundations can allow us to capture the essential aspects of reflective systems in a formalism-independent way. This paper proposes metalogical axioms for reflective logics and declarative languages based on the theory of general logics. In this way, several strands of work in reflection, including functional, equational, Horn logic, and rewriting logic reflective languages, as well as a variety of reflective theorem proving systems are placed within a common theoretical framework. General axioms for computational strategies, and for the internalization of those strategies in a reflective logic are also given.

Mesguer@csl.sri.com
clavel@csl.sri.com


Click here to get Aladdin Ghostscript 5.10.

Click here to get Adobe Acrobat Reader 3.01.



Home

Overview

Table of Contents

Author Index

Credits



Last Update: 06/28/98
Web Author: Matthew Hurlbut
hurlbut@jerry.cs.uiuc.edu