Reflective reasoning with and between a declarative metatheory and the implementation code

摘要

The goal of this paper is to present a theorem prover where the underlying code has been written to behave as the procedural met-alevel of the object logic. We have then defined a logical declarative metatheory MT which can be put in a one-to-one relation with the code and automatically generated from it. MT is proved correct and complete in the sense that, for any object level deduction, the wff representing it is a theorem of MT, and viceversa. Such theorems can be translated back in the underlying code. This opens up the possibility of deriving control strategies automatically by metatheoretic theorem proving, of mapping them into the code and thus of extending and modifying the system itself. This seems a first step towards "really" self-reflective systems, ie. systems able to reason deductively about and modify their underlying computation mechanisms. We show that the usual logical reflection rules (so called reflection up and down) are derived inference rules of the system.