COMPUTATIONAL REFLECTION VIA MECHANIZED LOGICAL DEDUCTION

In this article, we show how a system for automated deduction can be g iven computational reflection, i.e., can affect its own computation me chanism, by using the very same machinery implementing logical deducti on. This feature, which we call computational reflection via mechanize d logical deduction, provides both theoretical and practical advantage s. First, the theorem prover can inspect, extend, and modify its own u nderlying theorem-proving strategies automatically. Second, mechanized logical deduction can be used to reason about the ways these strategi es can be extended and modified and to prove correctness statements. T his opens up the possibility of building systems that are able to perf orm correct and safe, reflective self-extension and self-modification. (C) 1996 John Wiley & Sons, Inc.