A Tagged LCF-style Proof Architecture
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.