In this appendix, we formalize a specific annotation calculus that is able to deal with all the examples that we have presented in Chapter 6. This calculus is based on a first-order proof calculus and a corresponding unification procedure.

We wish to emphasize that the approach presented is an example of a more general technique to combine annotations and logic calculi. Another example is Hutter & Kohlhase (2000), which describes how to incorporate annotations into a calculus based on higher-order logic. Both approaches share the same principal mechanisms to incorporate annotations into calculi.

An annotation calculus

The integration of annotations into a calculus is determined by the definition of annotated substitution, which we have only sketched in Section 6.1. As seen in Section 6.2.3, annotated substitutions instantiate both meta-variables and annotation variables. Note that, in contrast to the formalization in Chapter 4, instantiations of meta-variables are independent of instantiations of annotations, since we have separated signatures and variables for annotation terms and object terms.

To cope with these different kinds of variables, an annotated substitution consists of a substitution for meta-variables as well as a family of substitutions for annotation variables. The definition of annotated substitutions determines the possible ways to inherit information during an inference step. To guarantee that an annotated inference step corresponds to a sound inference step in the non-annotated calculus, an annotated substitution has to denote a “standard” substitution if we erase all annotations.