# A Tagged LCF-style Proof Architecture

# Abstract

We describe the notion of *tagged inference* as it arises in
LCF-style theorem proving systems. Adding tags considerably widens the
applicability of such systems, while costing little. By way of
introduction, we give a simple tagged implementation of a propositional
logic. We also discuss how tagged inference is currently used in an
industrial strength proof system. Some knowledge of ML is assumed.
paper