Annotated reasoning
The application of deduction in various domains resulted in a variety of different techniques to guide the proof search. Many of these techniques incorporate 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 constituents of formulas and illustrate how a generic method of inheriting these annotations can br instantiated for various purposes.
automated deduction tactical theorem proving strategies rippling