Annotated reasoning

The application of deduction in various domains resulted in a variety of di fferent techniques to guide the proof search. Many of these techniques inco rporate additional knowledge to restrict or select possible proof steps. As a consequence, usually the underlying calculus has to he modified to keep track of this information during the proof search. In this paper we present a general framework fur maintaining additional strategic knowledge within a proof. We introduce a formal notion of annotations attached to the consti tuents of formulas and illustrate how a generic method of inheriting these annotations can br instantiated for various purposes.